Commit 2022-03-05 00:00 8e1da4e6

View on Github →

feat(ring_theory/adjoin/basic): if a set of elements of a subobject commute, its closure/adjoin is also commutative (#12231) We show that if a set of elements of a subobject commute, its closure/adjoin is also commutative The subobjects include (additive) submonoids, (additive) subgroups, subsemirings, subrings, and subalgebras.

Estimated changes

Modified src/group_theory/subgroup/basic.lean

added def subgroup.closure_comm_group_of_comm

added theorem subgroup.closure_induction₂

Modified src/group_theory/submonoid/basic.lean

added theorem submonoid.closure_induction₂

Modified src/group_theory/submonoid/membership.lean

added def submonoid.closure_comm_monoid_of_comm

Modified src/ring_theory/adjoin/basic.lean

added def algebra.adjoin_comm_ring_of_comm

added def algebra.adjoin_comm_semiring_of_comm

added theorem algebra.adjoin_induction₂

Modified src/ring_theory/subring/basic.lean

added def subring.closure_comm_ring_of_comm

added theorem subring.closure_induction₂

Modified src/ring_theory/subsemiring/basic.lean

added def subsemiring.closure_comm_semiring_of_comm

added theorem subsemiring.closure_induction₂