Commit 2019-10-03 09:33 4bb8d447

feat(data/equiv/algebra): automorphism groups for other structures (#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 [email protected]
• Update src/data/equiv/algebra.lean Co-Authored-By: Chris Hughes [email protected]
• Update src/data/equiv/algebra.lean Co-Authored-By: Chris Hughes [email protected]
• Update src/data/equiv/algebra.lean Co-Authored-By: Chris Hughes [email protected]
• Update src/data/equiv/algebra.lean Co-Authored-By: Chris Hughes [email protected]
• Update src/data/equiv/algebra.lean Co-Authored-By: Chris Hughes [email protected]
• Update src/data/equiv/algebra.lean Co-Authored-By: Chris Hughes [email protected]
• Update src/data/equiv/algebra.lean Co-Authored-By: Chris Hughes [email protected]
• Update src/data/equiv/algebra.lean Co-Authored-By: Chris Hughes [email protected]
• 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