Theorems · Inductive type · linear algebra
Algebra.IsQuadraticExtension
(R : Type u_2) → (S : Type u_3) → [inst : CommSemiring R] → [StrongRankCondition R] → [inst_2 : Semiring S] → [Algebra R S] → Prop
An extension of rings R ⊆ S is quadratic if S is a free R-algebra of rank 2.
- Cited by
- 11 results in Mathlib
- Foundations
- Depth 2 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Semiringstatement · cited by 13,802
- Algebrastatement · cited by 11,388
- CommSemiringstatement · cited by 10,911
- StrongRankConditionstatement · cited by 286
Cited by16
Results whose statement or proof uses this declaration.
- Algebra.IsQuadraticExtension.finrank_eq_twostatement and proof · cited by 3
- NumberField.CMExtension.equivMaximalRealSubfieldstatement and proof · cited by 3
- Algebra.IsQuadraticExtension.finrank_eq_two'statement and proof · cited by 1
- NumberField.IsCMField.ofCMExtensionstatement and proof · cited by 1
- NumberField.CMExtension.equivMaximalRealSubfield_applystatement and proof · cited by 1
- NumberField.CMExtension.equivMaximalRealSubfield.congr_simpstatement and proof · cited by 0
- Algebra.IsQuadraticExtension.casesOnstatement and proof · cited by 0
- Algebra.IsQuadraticExtension.congr_simpstatement and proof · cited by 0
- Algebra.IsQuadraticExtension.isMulCommutative_galoisGroupstatement and proof · cited by 0
- Algebra.IsQuadraticExtension.recOnstatement and proof · cited by 0
- NumberField.IsCMField.is_quadraticstatement · cited by 0
- NumberField.IsCMField.of_forall_isConjproof · cited by 0