Theorems · Definition · ring theory
Subalgebra.centralizer
(R : Type u) →
{A : Type v} → [inst : CommSemiring R] → [inst_1 : Semiring A] → [inst_2 : Algebra R A] → Set A → Subalgebra R AThe centralizer of a set as a subalgebra.
- Defined in
- Mathlib.Algebra.Algebra.Subalgebra.Basic
- Cited by
- 25 results in Mathlib
- Foundations
- Depth 19 from the axioms · uses propext, Quot.sound
- Assumes
- CommSemiringSemiringAlgebra
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites8
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement and proof · cited by 53,352
- Semiringstatement and proof · cited by 13,802
- Algebrastatement and proof · cited by 11,388
- CommSemiringstatement and proof · cited by 10,911
- Subalgebrastatement · cited by 1,353
- Subsemiringproof · cited by 456
- Subsemiring.centralizerproof · cited by 13
- Set.algebraMap_mem_centralizerproof · cited by 0
Cited by26
Results whose statement or proof uses this declaration.
- StarSubalgebra.centralizerproof · cited by 9
- Algebra.adjoin_le_centralizer_centralizerstatement · cited by 3
- Subalgebra.centralizer_coe_image_includeLeft_eq_center_tensorProductstatement and proof · cited by 2
- Subalgebra.centralizer_univstatement · cited by 2
- StarAlgebra.adjoin_le_centralizer_centralizerproof · cited by 2
- Subalgebra.le_centralizer_iffstatement and proof · cited by 2
- Subalgebra.topologicalClosure_adjoin_le_centralizer_centralizerstatement and proof · cited by 1
- Subalgebra.mem_centralizer_iffstatement · cited by 1
- Subalgebra.centralizer_coe_image_includeRight_eq_center_tensorProductstatement and proof · cited by 1
- Subalgebra.centralizer_coe_map_includeLeft_eq_center_tensorProductstatement · cited by 1
- Subalgebra.centralizer_coe_map_includeRight_eq_center_tensorProductstatement · cited by 1
- Subalgebra.centralizer_coe_range_includeLeft_eq_center_tensorProductstatement and proof · cited by 1