Structures · Algebra
SubfieldClass
SubfieldClass S K states S is a type of subsets s ⊆ K closed under field operations.
- Defined in
- Mathlib.Algebra.Field.Subfield.Defs
- Shape
- 2 explicit arguments
Extends2
Extended by0
Nothing extends this class yet.
Concrete types that are instances2
- IntermediateField
- Subfield
How is a type an instance?
Loading the hierarchy index…
Assumed by19
- SubfieldClass.ratCast_mem
- SubfieldClass.nnratCast_mem
- SubfieldClass.coe_ratCast
- SubfieldClass.coe_nnratCast
- SubfieldClass.instNNRatCast
- SubfieldClass.toSubringClass
- SubfieldClass.toField
- SubfieldClass.toInvMemClass
- SubfieldClass.toDivisionRing
- SubfieldClass.instRatCast
- SubfieldClass.qsmul_mem
- SubfieldClass.toSubgroupClass
- SubfieldClass.coe_nnqsmul
- SubfieldClass.instSMulNNRat
- SubfieldClass.ofScientific_mem
- SubfieldClass.nnqsmul_mem
- SubfieldClass.instSMulRat
- SubfieldClass.coe_qsmul
- SubfieldClass.toNormedField