Structures · Algebra
Algebra.IsQuadraticExtension
An extension of rings R ⊆ S is quadratic if S is a free R-algebra of rank 2.
- Shape
- 2 explicit arguments · adds finrank_eq_two'
Extends1
Extended by0
Nothing extends this class yet.
Concrete types that are instances1
- Subtype
How is a type an instance?
Loading the hierarchy index…
Assumed by14
- NumberField.CMExtension.equivMaximalRealSubfield
- Algebra.IsQuadraticExtension.finrank_eq_two
- Algebra.IsQuadraticExtension.finrank_eq_two'
- NumberField.IsCMField.ofCMExtension
- NumberField.CMExtension.equivMaximalRealSubfield_apply
- Algebra.IsQuadraticExtension.isCyclic
- NumberField.CMExtension.eq_maximalRealSubfield
- Algebra.instFiniteOfIsQuadraticExtension
- NumberField.CMExtension.algebraMap_equivMaximalRealSubfield_symm_apply
- Algebra.IsQuadraticExtension.isGalois
- Algebra.IsQuadraticExtension.toFree
- NumberField.CMExtension.equivMaximalRealSubfield.congr_simp
- Algebra.IsQuadraticExtension.normal
- Algebra.IsQuadraticExtension.isMulCommutative_galoisGroup