Skip to content

Tags: Ruben-VandeVelde/mathlib

Tags

snapshot-2019-10

Toggle snapshot-2019-10's commit message
feat(data/equiv/algebra): automorphism groups for other structures (l…

…eanprover-community#1141)

* Added automorphism groups to data/algebra/lean

* feat(data/equiv/algebra):
added automorphism groups

* feat(data/equiv/algebra)
Added automorphism groups

* Minor formatting

* feat(data/equiv/algebra):  add automorphism groups

* Changes based on comments

* minor change

* changes to namespaces and comments added

* expanding comments

* Update src/data/equiv/algebra.lean

Co-Authored-By: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com>

* Update src/data/equiv/algebra.lean

Co-Authored-By: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com>

* Update src/data/equiv/algebra.lean

Co-Authored-By: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com>

* Update src/data/equiv/algebra.lean

Co-Authored-By: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com>

* Update src/data/equiv/algebra.lean

Co-Authored-By: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com>

* Update src/data/equiv/algebra.lean

Co-Authored-By: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com>

* Update src/data/equiv/algebra.lean

Co-Authored-By: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com>

* Update src/data/equiv/algebra.lean

Co-Authored-By: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com>

* Update src/data/equiv/algebra.lean

Co-Authored-By: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com>

* Added monoid case

* Changed Type to Type* also further up in the file

* typo

* I made it compile but not pretty

* More changes

* fixed typo

* fix universes

* update docs

* minor change

* use coercion rather than to_fun in ext lemmas

* Use ≃+* and coercion in ring_equiv.ext

* arguments of group.aut?

* generalize ring_equiv.ext to semirings

* Various changes

* Use only `mul_aut`, `add_aut`, and `ring_aut` for automorphisms.

* Make `*_equiv.ext` arguments agree with `equiv.ext`.

* Adjust documentation.

* Fix compile, add `add_aut.to_perm`