tag:github.com,2008:https://github.com/lacker/mathlib/releasesTags from mathlib2019-10-03T09:33:33Ztag:github.com,2008:Repository/298686743/snapshot-2019-102019-10-03T09:33:33Zsnapshot-2019-10<p>feat(data/equiv/algebra): automorphism groups for other structures (<a class="issue-link js-issue-link" href="https://github.com/leanprover-community/mathlib3/pull/1141">l…</a></p>
<p><a class="issue-link js-issue-link" href="https://github.com/leanprover-community/mathlib3/pull/1141">…eanprover-community#1141</a>)</p>
<p>* Added automorphism groups to data/algebra/lean</p>
<p>* feat(data/equiv/algebra):
<br />added automorphism groups</p>
<p>* feat(data/equiv/algebra)
<br />Added automorphism groups</p>
<p>* Minor formatting</p>
<p>* feat(data/equiv/algebra): add automorphism groups</p>
<p>* Changes based on comments</p>
<p>* minor change</p>
<p>* changes to namespaces and comments added</p>
<p>* expanding comments</p>
<p>* Update src/data/equiv/algebra.lean</p>
<p>Co-Authored-By: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com></p>
<p>* Update src/data/equiv/algebra.lean</p>
<p>Co-Authored-By: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com></p>
<p>* Update src/data/equiv/algebra.lean</p>
<p>Co-Authored-By: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com></p>
<p>* Update src/data/equiv/algebra.lean</p>
<p>Co-Authored-By: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com></p>
<p>* Update src/data/equiv/algebra.lean</p>
<p>Co-Authored-By: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com></p>
<p>* Update src/data/equiv/algebra.lean</p>
<p>Co-Authored-By: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com></p>
<p>* Update src/data/equiv/algebra.lean</p>
<p>Co-Authored-By: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com></p>
<p>* Update src/data/equiv/algebra.lean</p>
<p>Co-Authored-By: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com></p>
<p>* Update src/data/equiv/algebra.lean</p>
<p>Co-Authored-By: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com></p>
<p>* Added monoid case</p>
<p>* Changed Type to Type* also further up in the file</p>
<p>* typo</p>
<p>* I made it compile but not pretty</p>
<p>* More changes</p>
<p>* fixed typo</p>
<p>* fix universes</p>
<p>* update docs</p>
<p>* minor change</p>
<p>* use coercion rather than to_fun in ext lemmas</p>
<p>* Use ≃+* and coercion in ring_equiv.ext</p>
<p>* arguments of group.aut?</p>
<p>* generalize ring_equiv.ext to semirings</p>
<p>* Various changes</p>
<p>* Use only `mul_aut`, `add_aut`, and `ring_aut` for automorphisms.</p>
<p>* Make `*_equiv.ext` arguments agree with `equiv.ext`.</p>
<p>* Adjust documentation.</p>
<p>* Fix compile, add `add_aut.to_perm`</p>callum-sutton