Centralizer

📁 Source: Mathlib/Algebra/Algebra/Subalgebra/Centralizer.lean

Statistics

Metric	Count
Definitions	0
Theorems centralizer_coe_iSup, centralizer_coe_image_includeLeft_eq_center_tensorProduct, centralizer_coe_image_includeRight_eq_center_tensorProduct, centralizer_coe_map_includeLeft_eq_center_tensorProduct, centralizer_coe_map_includeRight_eq_center_tensorProduct, centralizer_coe_range_includeLeft_eq_center_tensorProduct, centralizer_coe_sup, centralizer_range_includeRight_eq_center_tensorProduct, centralizer_tensorProduct_eq_center_tensorProduct_left, centralizer_tensorProduct_eq_center_tensorProduct_right, le_centralizer_iff	11
Total	11

Subalgebra

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
centralizer_coe_iSup 📖	mathematical	—	centralizer SetLike.coe Subalgebra instSetLike iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice Algebra.instCompleteLatticeSubalgebra iInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf	—	eq_of_forall_le_iff le_centralizer_iff
centralizer_coe_image_includeLeft_eq_center_tensorProduct 📖	mathematical	—	centralizer TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule Algebra.TensorProduct.instSemiring Algebra.TensorProduct.leftAlgebra IsScalarTower.to_smulCommClass CommSemiring.toSemiring Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction Set.image DFunLike.coe AlgHom smulCommClass_self CommSemiring.toCommMonoid CommMonoid.toMonoid AlgHom.funLike Algebra.TensorProduct.includeLeft AlgHom.range Subalgebra SetLike.instMembership instSetLike toSemiring algebra instIsScalarTowerSubtypeMem Algebra.toSMul Algebra.TensorProduct.map val AlgHom.id	—	ext IsScalarTower.to_smulCommClass IsScalarTower.left smulCommClass_self instIsScalarTowerSubtypeMem TensorProduct.eq_repr_basis_right sum_mem mem_centralizer_iff MulZeroClass.zero_mul TensorProduct.sum_tmul_basis_right_injective RingHomInvPair.ids TensorProduct.smulCommClass_left SMulCommClass.symm Finsupp.sum_of_support_subset Finsupp.support_smul map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass Finsupp.support_mapRange Finset.sum_congr Algebra.to_smulCommClass IsScalarTower.right Finset.mul_sum one_mul Finset.sum_mul mul_one Finsupp.ext_iff TensorProduct.induction_on MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass AlgHom.algHomClass MulZeroClass.mul_zero map_add AddMonoidHomClass.toAddHomClass RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass mul_add Distrib.leftDistribClass add_mul Distrib.rightDistribClass
centralizer_coe_image_includeRight_eq_center_tensorProduct 📖	mathematical	—	centralizer TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule Algebra.TensorProduct.instSemiring Algebra.TensorProduct.leftAlgebra IsScalarTower.to_smulCommClass CommSemiring.toSemiring Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction Set.image DFunLike.coe AlgHom Algebra.TensorProduct.instAlgebra AlgHom.funLike Algebra.TensorProduct.includeRight AlgHom.range Subalgebra SetLike.instMembership instSetLike toSemiring algebra Algebra.TensorProduct.map AlgHom.id val	—	IsScalarTower.to_smulCommClass IsScalarTower.left smulCommClass_self instIsScalarTowerSubtypeMem centralizer_coe_image_includeLeft_eq_center_tensorProduct ext Set.image_congr AlgEquivClass.toAlgHomClass AlgEquiv.instAlgEquivClass AlgEquiv.injective Algebra.to_smulCommClass IsScalarTower.right map_mul NonUnitalAlgSemiHomClass.toMulHomClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgEquiv.symm_apply_apply Algebra.TensorProduct.comm_comp_map_apply Algebra.TensorProduct.comm_symm
centralizer_coe_map_includeLeft_eq_center_tensorProduct 📖	mathematical	—	centralizer TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule Algebra.TensorProduct.instSemiring Algebra.TensorProduct.leftAlgebra IsScalarTower.to_smulCommClass CommSemiring.toSemiring Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction SetLike.coe Subalgebra instSetLike map Algebra.TensorProduct.includeLeft AlgHom.range SetLike.instMembership toSemiring algebra instIsScalarTowerSubtypeMem Algebra.toSMul Algebra.TensorProduct.map val AlgHom.id	—	centralizer_coe_image_includeLeft_eq_center_tensorProduct
centralizer_coe_map_includeRight_eq_center_tensorProduct 📖	mathematical	—	centralizer TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule Algebra.TensorProduct.instSemiring Algebra.TensorProduct.leftAlgebra IsScalarTower.to_smulCommClass CommSemiring.toSemiring Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction SetLike.coe Subalgebra Algebra.TensorProduct.instAlgebra instSetLike map Algebra.TensorProduct.includeRight AlgHom.range SetLike.instMembership toSemiring algebra Algebra.TensorProduct.map AlgHom.id val	—	centralizer_coe_image_includeRight_eq_center_tensorProduct
centralizer_coe_range_includeLeft_eq_center_tensorProduct 📖	mathematical	—	centralizer TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule Algebra.TensorProduct.instSemiring Algebra.TensorProduct.leftAlgebra IsScalarTower.to_smulCommClass CommSemiring.toSemiring Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction SetLike.coe Subalgebra instSetLike AlgHom.range Algebra.TensorProduct.includeLeft SetLike.instMembership center toSemiring algebra instIsScalarTowerSubtypeMem Algebra.toSMul Algebra.TensorProduct.map val AlgHom.id	—	IsScalarTower.to_smulCommClass IsScalarTower.left instIsScalarTowerSubtypeMem centralizer_univ Algebra.coe_top centralizer_coe_map_includeLeft_eq_center_tensorProduct ext Algebra.to_smulCommClass IsScalarTower.right Algebra.map_top
centralizer_coe_sup 📖	mathematical	—	centralizer SetLike.coe Subalgebra instSetLike SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Algebra.instCompleteLatticeSubalgebra SemilatticeInf.toMin Lattice.toSemilatticeInf	—	eq_of_forall_le_iff le_centralizer_iff
centralizer_range_includeRight_eq_center_tensorProduct 📖	mathematical	—	centralizer TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule Algebra.TensorProduct.instSemiring Algebra.TensorProduct.leftAlgebra IsScalarTower.to_smulCommClass CommSemiring.toSemiring Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction SetLike.coe Subalgebra Algebra.TensorProduct.instAlgebra instSetLike AlgHom.range Algebra.TensorProduct.includeRight SetLike.instMembership center toSemiring algebra Algebra.TensorProduct.map AlgHom.id val	—	IsScalarTower.to_smulCommClass IsScalarTower.left centralizer_univ Algebra.coe_top centralizer_coe_map_includeRight_eq_center_tensorProduct ext Algebra.map_top
centralizer_tensorProduct_eq_center_tensorProduct_left 📖	mathematical	—	centralizer TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule Algebra.TensorProduct.instSemiring Algebra.TensorProduct.leftAlgebra IsScalarTower.to_smulCommClass CommSemiring.toSemiring Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction SetLike.coe Subalgebra instSetLike AlgHom.range Algebra.TensorProduct.map AlgHom.id Algebra.ofId SetLike.instMembership center toSemiring algebra instIsScalarTowerSubtypeMem Algebra.toSMul val	—	IsScalarTower.to_smulCommClass IsScalarTower.left instIsScalarTowerSubtypeMem centralizer_coe_range_includeLeft_eq_center_tensorProduct Algebra.TensorProduct.map_range Algebra.comp_ofId sup_of_le_left
centralizer_tensorProduct_eq_center_tensorProduct_right 📖	mathematical	—	centralizer TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule Algebra.TensorProduct.instSemiring Algebra.TensorProduct.leftAlgebra IsScalarTower.to_smulCommClass CommSemiring.toSemiring Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction SetLike.coe Subalgebra instSetLike AlgHom.range IsScalarTower.right Algebra.TensorProduct.map Algebra.ofId AlgHom.id SetLike.instMembership center toSemiring algebra val	—	IsScalarTower.to_smulCommClass IsScalarTower.left IsScalarTower.right centralizer_range_includeRight_eq_center_tensorProduct Algebra.TensorProduct.map_range Algebra.comp_ofId sup_of_le_right
le_centralizer_iff 📖	mathematical	—	Subalgebra Preorder.toLE PartialOrder.toPreorder instPartialOrder centralizer SetLike.coe instSetLike	—	—

---

← Back to Index