Structures · Algebra
Algebra.IsCentral
For a commutative ring K and a K-algebra D, we say that D is a central algebra over K if
the center of D is the image of K in D.
- Defined in
- Mathlib.Algebra.Central.Defs
- Shape
- 2 explicit arguments · adds out
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances0
No instance on a concrete type; it is reached through other classes.
How is a type an instance?
Loading the hierarchy index…
Assumed by18
- Algebra.IsCentral.center_eq_bot
- Algebra.IsCentral.out
- Algebra.IsCentral.left_of_tensor
- Algebra.IsCentral.of_algEquiv
- LinearEquiv.conjAlgEquiv_ext_iff
- Algebra.IsCentral.right_of_tensor
- Unitary.conjStarAlgAut_ext_iff'
- JacobsonNoether.exists_separable_and_not_isCentral'
- Unitary.conjStarAlgAut_ext_iff
- Algebra.IsCentral.mem_center_iff
- Algebra.IsCentral.instMulOpposite
- LinearEquiv.conjAlgEquiv_ext_iff'
- Algebra.IsCentral.matrix
- Algebra.IsCentral.left_of_tensor_of_field
- Algebra.IsCentral.baseField_essentially_unique
- Algebra.IsCentral.instEnd
- Algebra.IsCentral.right_of_tensor_of_field
- Algebra.IsCentral.instContinuousLinearMap
Ancestors0
No ancestors.