Tags: Ruben-VandeVelde/mathlib
Tags
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`