Basic

📁 Source: Mathlib/Algebra/Central/Basic.lean

Statistics

Metric	Count
Definitions	0
Theorems baseField_essentially_unique, center_eq_bot, instMulOpposite, mem_center_iff, of_algEquiv, self	6
Total	6

Algebra.IsCentral

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
baseField_essentially_unique 📖	mathematical	—	Function.Bijective DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring RingHom.instFunLike algebraMap	—	FaithfulSMul.algebraMap_injective Module.IsTorsionFree.to_faithfulSMul IsDomain.toIsCancelMulZero Field.isDomain IsSimpleRing.instNontrivial DivisionRing.isSimpleRing DivisionSemiring.to_moduleIsTorsionFree Subalgebra.algebraMap_mem center_eq_bot RingHom.injective Algebra.algebraMap_eq_smul_one smul_assoc one_smul
center_eq_bot 📖	mathematical	—	Subalgebra.center Bot.bot Subalgebra OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice Algebra.instCompleteLatticeSubalgebra BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder	—	eq_bot_iff out
instMulOpposite 📖	mathematical	—	Algebra.IsCentral MulOpposite MulOpposite.instSemiring MulOpposite.instAlgebra	—	out MulOpposite.unop_mem_center_iff
mem_center_iff 📖	mathematical	—	Subalgebra SetLike.instMembership Subalgebra.instSetLike Subalgebra.center DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike algebraMap	—	center_eq_bot Algebra.mem_bot
of_algEquiv 📖	mathematical	—	Algebra.IsCentral	—	out MulEquivClass.apply_mem_center_iff RingEquivClass.toMulEquivClass AlgEquivClass.toRingEquivClass AlgEquiv.instAlgEquivClass AlgEquiv.commutes AlgEquiv.apply_symm_apply
self 📖	mathematical	—	Algebra.IsCentral CommSemiring.toSemiring Algebra.id	—	Subalgebra.center_eq_top Set.range_id

---

← Back to Index