Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-15 16:38 7ed4f2ce

View on Github →

feat(group_theory/submonoid/operations): monoids are isomorphic to themselves as submonoids (#12658)

Estimated changes

Modified src/algebra/algebra/subalgebra/basic.lean

deleted def algebra.top_equiv

added def subalgebra.top_equiv

Modified src/algebra/lie/nilpotent.lean

Modified src/algebra/lie/semisimple.lean

Modified src/algebra/lie/solvable.lean

Modified src/algebra/lie/submodule.lean

added def lie_ideal.top_equiv

added theorem lie_ideal.top_equiv_apply

deleted def lie_ideal.top_equiv_self

deleted theorem lie_ideal.top_equiv_self_apply

added def lie_subalgebra.top_equiv

added theorem lie_subalgebra.top_equiv_apply

deleted def lie_subalgebra.top_equiv_self

deleted theorem lie_subalgebra.top_equiv_self_apply

Modified src/algebra/module/submodule_lattice.lean

added def submodule.top_equiv

deleted def submodule.top_equiv_self

Modified src/field_theory/adjoin.lean

Modified src/group_theory/subgroup/basic.lean

added def subgroup.top_equiv

Modified src/group_theory/submonoid/operations.lean

added def submonoid.top_equiv

added theorem submonoid.top_equiv_to_monoid_hom

Modified src/number_theory/cyclotomic/primitive_roots.lean

Modified src/ring_theory/adjoin/power_basis.lean