Theorems · Inductive type · field theory
Subfield
(K : Type u) → [DivisionRing K] → Type u
Subfield R is the type of subfields of R. A subfield of R is a subset s that is a
multiplicative submonoid and an additive subgroup. Note in particular that it shares the
same 0 and 1 as R.
- Defined in
- Mathlib.Algebra.Field.Subfield.Defs
- Cited by
- 303 results in Mathlib
- Foundations
- Depth 1 from the axioms, rests on 2 definitions · uses no axioms
- Assumes
- DivisionRing
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DivisionRingstatement · cited by 1,062
Cited by356
Results whose statement or proof uses this declaration.
- IntermediateField.adjoinproof · cited by 382
- IntermediateField.restrictScalarsproof · cited by 66
- AlgHom.fieldRangeproof · cited by 57
- RingHom.fieldRangestatement · cited by 40
- Subfield.relrankstatement and proof · cited by 40
- Subfield.closurestatement and proof · cited by 39
- IntermediateField.toSubfieldstatement · cited by 38
- NumberField.maximalRealSubfieldstatement · cited by 38
- Subfield.mapstatement and proof · cited by 30
- Subfield.comapstatement and proof · cited by 29
- Subfield.relfinrankstatement and proof · cited by 23
- Subfield.toSubringstatement and proof · cited by 23
Showing the 200 most cited of 356.