Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-06-07 19:34 b915e939

View on Github →

feat(ring_theory/subring): centralizer as a subring (#18861)

Estimated changes

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

added theorem subalgebra.center_le_centralizer

added theorem subalgebra.centralizer_eq_top_iff_subset

Modified src/group_theory/subgroup/basic.lean

added theorem subgroup.center_le_centralizer

added theorem subgroup.centralizer_eq_top_iff_subset

Modified src/group_theory/submonoid/centralizer.lean

added theorem submonoid.center_le_centralizer

added theorem submonoid.centralizer_eq_top_iff_subset

Modified src/group_theory/subsemigroup/centralizer.lean

added theorem set.center_subset_centralizer

added theorem set.centralizer_eq_top_iff_subset

added theorem subsemigroup.center_le_centralizer

added theorem subsemigroup.centralizer_eq_top_iff_subset

Modified src/ring_theory/non_unital_subsemiring/basic.lean

added theorem non_unital_subsemiring.center_le_centralizer

added theorem non_unital_subsemiring.centralizer_eq_top_iff_subset

Modified src/ring_theory/subring/basic.lean

added theorem subring.center_le_centralizer

added def subring.centralizer

added theorem subring.centralizer_eq_top_iff_subset

added theorem subring.centralizer_le

added theorem subring.centralizer_to_submonoid

added theorem subring.centralizer_to_subsemiring

added theorem subring.centralizer_univ

added theorem subring.coe_centralizer

added theorem subring.mem_centralizer_iff

Modified src/ring_theory/subsemiring/basic.lean

added theorem subsemiring.center_le_centralizer

added theorem subsemiring.centralizer_eq_top_iff_subset