Defs

📁 Source: Mathlib/Algebra/Field/Subfield/Defs.lean

Statistics

Metric	Count
Definitions `copy`, `instDivSubtypeMem`, `instInvSubtypeMem`, `instPartialOrder`, `instPowSubtypeMemInt`, `instRingSubtypeMem`, `instSetLike`, `subtype`, `toAddSubgroup`, `toDivisionRing`, `toField`, `toSubring`, `SubfieldClass`, `instNNRatCast`, `instRatCast`, `instSMulNNRat`, `instSMulRat`, `toDivisionRing`, `toField`, `toSubfield`	20
Theorems `add_mem`, `coe_add`, `coe_copy`, `coe_div`, `coe_inv`, `coe_mul`, `coe_neg`, `coe_one`, `coe_set_mk`, `coe_sub`, `coe_subtype`, `coe_toAddSubgroup`, `coe_toSubmonoid`, `coe_toSubring`, `coe_zero`, `copy_eq`, `div_mem`, `ext`, `ext_iff`, `instSubfieldClass`, `intCast_mem`, `inv_mem`, `inv_mem'`, `mem_carrier`, `mem_mk`, `mem_toAddSubgroup`, `mem_toSubmonoid`, `mem_toSubring`, `mk_le_mk`, `mul_mem`, `neg_mem`, `one_mem`, `pow_mem`, `sub_mem`, `subtype_apply`, `subtype_injective`, `toSubring_subtype_eq_subtype`, `zero_mem`, `zpow_mem`, `zsmul_mem`, `coe_nnqsmul`, `coe_nnratCast`, `coe_qsmul`, `coe_ratCast`, `nnqsmul_mem`, `nnratCast_mem`, `ofScientific_mem`, `qsmul_mem`, `ratCast_mem`, `toInvMemClass`, `toSubgroupClass`, `toSubringClass`	52
Total	72

Subfield

Definitions

Name	Category	Theorems
`copy` 📖	CompOp	2 math math: `copy_eq`, `coe_copy`
`instDivSubtypeMem` 📖	CompOp	1 math math: `coe_div`
`instInvSubtypeMem` 📖	CompOp	1 math math: `coe_inv`
`instPartialOrder` 📖	CompOp	24 math math: `IntermediateField.fieldRange_le`, `relfinrank_eq_one_iff`, `closure_le`, `mk_le_mk`, `closure_mono`, `extendScalars_le_extendScalars_iff`, `gc_map_comap`, `topologicalClosure_minimal`, `extendScalars.orderIso_symm_apply`, `NumberField.isTotallyReal_iff_le_maximalRealSubfield`, `extendScalars_top`, `le_extendScalars_iff`, `extendScalars_le_iff`, `extendScalars.orderIso_apply`, `map_le_iff_le_comap`, `closure_preimage_le`, `IntermediateField.adjoin_le_subfield`, `NumberField.IsTotallyReal.le_maximalRealSubfield`, `relrank_eq_one_iff`, `extendScalars_self`, `RingHom.field_closure_preimage_le`, `isGLB_sInf`, `le_topologicalClosure`, `extendScalars_injective`
`instPowSubtypeMemInt` 📖	CompOp	—
`instRingSubtypeMem` 📖	CompOp	10 math math: `coe_add`, `splits_bot`, `coe_mul`, `roots_X_pow_char_sub_X_bot`, `RingHom.rangeRestrictFieldEquiv_apply_symm_apply`, `FixedPoints.smul_polynomial`, `charP`, `expChar`, `FixedPoints.smul`, `RingHom.rangeRestrictFieldEquiv_apply_coe`
`instSetLike` 📖	CompOp	190 math math: `ext_iff`, `FixedPoints.instFiniteDimensionalSubtypeMemSubfieldSubfield`, `Polynomial.Splits.mem_subfield_of_isRoot`, `rank_comap`, `FixedPoints.finrank_eq_card`, `FixedPoints.minpoly.monic`, `HahnSeries.mem_cardSuppLTSubfield`, `FixedPoints.minpoly.irreducible`, `mem_sSup_of_directedOn`, `add_mem`, `mem_sInf`, `NumberField.IsCMField.isConj_complexConj`, `NumberField.IsCMField.zpowers_complexConj_eq_top`, `coe_add`, `NumberField.instIsTotallyRealSubtypeMemSubfieldOfIsAlgebraic`, `zsmul_mem`, `closure_le`, `mem_toSubring`, `FixedPoints.isSeparable`, `NumberField.IsCMField.equivInfinitePlace_symm_apply`, `NumberField.IsCMField.units_rank_eq_units_rank`, `NumberField.mem_maximalRealSubfield_iff`, `multiset_prod_mem`, `NumberField.CMExtension.algebraMap_equivMaximalRealSubfield_symm_apply`, `FixedPoints.minpoly.eval₂'`, `mem_top`, `relfinrank_mul_finrank_top`, `RingHom.mem_fieldRange_self`, `extendScalars_toSubfield`, `relfinrank_eq_finrank_of_le`, `coe_top`, `coe_iSup_of_directed`, `splits_bot`, `coe_mul`, `cardinalMk_closure_le_max`, `NumberField.isTotallyReal_sup`, `mem_closure`, `FixedPoints.rank_le_card`, `coe_toIntermediateField`, `NumberField.isTotallyReal_top_iff`, `relrank_mul_rank_top`, `IntermediateField.subset_adjoin_of_subset_left`, `NumberField.IsCMField.isQuadraticExtension`, `instSubfieldClass`, `RingHom.eqOn_field_closure`, `NumberField.IsCMField.orderOf_complexConj`, `mem_bot_iff_pow_eq_self`, `coe_inv`, `isTotallyReal_bot`, `NumberField.IsCMField.regulator_div_regulator_eq_two_pow_mul_indexRealUnits_inv`, `list_prod_mem`, `coe_zero`, `mem_closure_iff`, `IntermediateField.coe_type_toSubfield`, `smulCommClass_left`, `FixedPoints.instSMulCommClassSubtypeMemSubfieldSubfield`, `RingHom.coe_rangeRestrictField`, `extendScalars_le_extendScalars_iff`, `FixedPoints.normal`, `extendScalars_inf`, `finrank_comap`, `mem_inf`, `NumberField.instIsTotallyRealSubtypeMemSubfieldTop`, `FixedPoints.finrank_le_card`, `smul_def`, `mem_iInf`, `HahnSeries.cardSuppLTSubfield_carrier`, `sum_mem`, `NumberField.IsCMField.complexConj_apply_apply`, `mem_closure_of_mem`, `NumberField.of_subfield`, `zpow_mem`, `NumberField.IsCMField.coe_ringOfIntegersComplexConj`, `prod_mem`, `NumberField.IsCMField.equivInfinitePlace_apply`, `IntermediateField.mem_toSubfield`, `NumberField.IsCMField.is_quadratic`, `NumberField.isTotallyReal_iSup`, `NumberField.IsCMField.complexConj_apply_eq_self`, `algebraMap_ofSubfield`, `zero_mem`, `coe_iInf`, `NumberField.IsCMField.complexEmbedding_complexConj`, `coe_comap`, `sub_mem`, `extendScalars.orderIso_symm_apply`, `FixedPoints.minpoly.irreducible_aux`, `NumberField.CMExtension.equivMaximalRealSubfield_apply`, `NumberField.isTotallyReal_iff_le_maximalRealSubfield`, `subtype_apply`, `roots_X_pow_char_sub_X_bot`, `relfinrank_top_right`, `NumberField.IsCMField.card_infinitePlace_eq_card_infinitePlace`, `coe_one`, `smulCommClass_right`, `instFaithfulSMulSubtypeMem`, `extendScalars_top`, `IntermediateField.coe_toSubfield`, `cardinalMk_closure`, `coe_set_mk`, `continuousSMul`, `neg_mem`, `fieldRange_subtype`, `coe_subtype`, `multiset_sum_mem`, `pow_mem`, `mem_iSup_of_directed`, `NumberField.isTotallyReal_maximalRealSubfield`, `one_mem`, `coe_inf`, `inv_mem`, `list_sum_mem`, `le_extendScalars_iff`, `FixedPoints.toAlgAut_surjective`, `relrank_dvd_rank_top_of_le`, `FixedPoints.isIntegral`, `RingHom.coe_fieldRange`, `RingHom.rangeRestrictFieldEquiv_apply_symm_apply`, `mem_toAddSubgroup`, `mem_mk`, `FixedPoints.smul_polynomial`, `NumberField.IsCMField.ringOfIntegersComplexConj_eq_self_iff`, `extendScalars_le_iff`, `NumberField.IsCMField.mem_realUnits_iff`, `charP`, `coe_sInf`, `extendScalars.orderIso_apply`, `relrank_top_right`, `coe_toSubring`, `relrank_eq_rank_of_le`, `RingHom.rangeRestrictField_bijective`, `Complex.uniformContinuous_ringHom_eq_id_or_conj`, `NumberField.IsCMField.exists_isConj`, `map_mem_map`, `FixedPoints.toAlgHom_bijective`, `coe_copy`, `mem_bot_iff_intCast`, `isClosed_topologicalClosure`, `IsGaloisGroup.fixedPoints`, `Matrix.mem_subfield_of_mul_eq_one_of_mem_subfield_right`, `coe_sSup_of_directedOn`, `extendScalars_sup`, `relfinrank_dvd_finrank_top_of_le`, `mul_mem`, `closure_eq`, `NumberField.IsCMField.complexConj_eq_self_iff`, `expChar`, `mem_toSubmonoid`, `instIsScalarTowerSubtypeMem`, `lift_rank_comap`, `div_mem`, `FixedPoints.minpoly_eq_minpoly`, `NumberField.IsCMField.RingOfIntegers.complexConj_eq_self_iff`, `RingHom.mem_fieldRange`, `coe_div`, `subset_closure`, `coe_toAddSubgroup`, `FixedPoints.toAlgAut_bijective`, `Matrix.mem_subfield_of_mul_eq_one_of_mem_subfield_left`, `FixedPoints.smul`, `NumberField.IsCMField.infinitePlace_complexConj`, `FixedPoints.smulCommClass'`, `RingHom.mem_eqLocusField`, `IsGalois.of_fixed_field`, `FixedPoints.coe_algebraMap`, `IsInvariantSubfield.smul_mem`, `card_bot`, `mem_map`, `RingHom.rangeRestrictFieldEquiv_apply_coe`, `coe_map`, `extendScalars_self`, `intCast_mem`, `mem_extendScalars`, `subtype_injective`, `completableTopField`, `coe_sub`, `NumberField.instIsAlgebraicSubtypeMemSubfield`, `NumberField.IsCMField.complexConj_torsion`, `mem_carrier`, `coe_neg`, `NumberField.IsCMField.Units.complexConj_eq_self_iff`, `toIsStrictOrderedRing`, `coe_toSubmonoid`, `coe_extendScalars`, `extendScalars_injective`, `NumberField.IsCMField.regOfFamily_realFunSystem`, `FixedPoints.minpoly.of_eval₂`, `mem_comap`, `FixedBy.subfield_mem_iff`, `IntermediateField.adjoin_contains_field_as_subfield`
`subtype` 📖	CompOp	9 math math: `FixedPoints.minpoly.eval₂'`, `algebraMap_ofSubfield`, `subtype_apply`, `fieldRange_subtype`, `coe_subtype`, `Complex.uniformContinuous_ringHom_eq_id_or_conj`, `toSubring_subtype_eq_subtype`, `FixedPoints.coe_algebraMap`, `subtype_injective`
`toAddSubgroup` 📖	CompOp	2 math math: `mem_toAddSubgroup`, `coe_toAddSubgroup`
`toDivisionRing` 📖	CompOp	9 math math: `FixedPoints.instFiniteDimensionalSubtypeMemSubfieldSubfield`, `RingHom.coe_rangeRestrictField`, `subtype_apply`, `continuousSMul`, `fieldRange_subtype`, `coe_subtype`, `RingHom.rangeRestrictField_bijective`, `Complex.uniformContinuous_ringHom_eq_id_or_conj`, `subtype_injective`
`toField` 📖	CompOp	73 math math: `rank_comap`, `FixedPoints.finrank_eq_card`, `FixedPoints.minpoly.monic`, `FixedPoints.minpoly.irreducible`, `NumberField.IsCMField.isConj_complexConj`, `NumberField.instIsTotallyRealSubtypeMemSubfieldOfIsAlgebraic`, `FixedPoints.isSeparable`, `NumberField.IsCMField.equivInfinitePlace_symm_apply`, `NumberField.IsCMField.units_rank_eq_units_rank`, `NumberField.CMExtension.algebraMap_equivMaximalRealSubfield_symm_apply`, `FixedPoints.minpoly.eval₂'`, `relfinrank_mul_finrank_top`, `extendScalars_toSubfield`, `relfinrank_eq_finrank_of_le`, `splits_bot`, `NumberField.isTotallyReal_sup`, `FixedPoints.rank_le_card`, `NumberField.isTotallyReal_top_iff`, `relrank_mul_rank_top`, `IntermediateField.subset_adjoin_of_subset_left`, `NumberField.IsCMField.isQuadraticExtension`, `isTotallyReal_bot`, `NumberField.IsCMField.regulator_div_regulator_eq_two_pow_mul_indexRealUnits_inv`, `extendScalars_le_extendScalars_iff`, `FixedPoints.normal`, `extendScalars_inf`, `finrank_comap`, `NumberField.instIsTotallyRealSubtypeMemSubfieldTop`, `FixedPoints.finrank_le_card`, `NumberField.of_subfield`, `NumberField.IsCMField.coe_ringOfIntegersComplexConj`, `NumberField.IsCMField.equivInfinitePlace_apply`, `NumberField.IsCMField.is_quadratic`, `NumberField.isTotallyReal_iSup`, `extendScalars.orderIso_symm_apply`, `FixedPoints.minpoly.irreducible_aux`, `NumberField.CMExtension.equivMaximalRealSubfield_apply`, `NumberField.isTotallyReal_iff_le_maximalRealSubfield`, `roots_X_pow_char_sub_X_bot`, `relfinrank_top_right`, `NumberField.IsCMField.card_infinitePlace_eq_card_infinitePlace`, `extendScalars_top`, `NumberField.isTotallyReal_maximalRealSubfield`, `le_extendScalars_iff`, `relrank_dvd_rank_top_of_le`, `FixedPoints.isIntegral`, `FixedPoints.smul_polynomial`, `NumberField.IsCMField.ringOfIntegersComplexConj_eq_self_iff`, `extendScalars_le_iff`, `NumberField.IsCMField.mem_realUnits_iff`, `extendScalars.orderIso_apply`, `relrank_top_right`, `relrank_eq_rank_of_le`, `Complex.uniformContinuous_ringHom_eq_id_or_conj`, `NumberField.IsCMField.exists_isConj`, `extendScalars_sup`, `relfinrank_dvd_finrank_top_of_le`, `lift_rank_comap`, `FixedPoints.minpoly_eq_minpoly`, `NumberField.IsCMField.RingOfIntegers.complexConj_eq_self_iff`, `FixedPoints.smul`, `IsGalois.of_fixed_field`, `extendScalars_self`, `mem_extendScalars`, `completableTopField`, `NumberField.instIsAlgebraicSubtypeMemSubfield`, `NumberField.IsCMField.Units.complexConj_eq_self_iff`, `toIsStrictOrderedRing`, `coe_extendScalars`, `extendScalars_injective`, `NumberField.IsCMField.regOfFamily_realFunSystem`, `FixedPoints.minpoly.of_eval₂`, `IntermediateField.adjoin_contains_field_as_subfield`
`toSubring` 📖	CompOp	12 math math: `mem_toSubring`, `subring_closure_le`, `coe_inf`, `sInf_toSubring`, `coe_toSubring`, `toSubring_subtype_eq_subtype`, `mem_toSubmonoid`, `mem_carrier`, `FixedPoints.minpoly.eval₂`, `inv_mem'`, `coe_toSubmonoid`, `instIsInvariantSubringOfIsInvariantSubfield`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_mem` 📖	mathematical	`Subfield` `SetLike.instMembership` `instSetLike`	`Subfield` `SetLike.instMembership` `instSetLike` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `DivisionRing.toRing`	—	`AddMemClass.add_mem` `AddSubmonoidClass.toAddMemClass` `AddSubgroupClass.toAddSubmonoidClass` `SubringClass.addSubgroupClass` `SubfieldClass.toSubringClass` `instSubfieldClass`
`coe_add` 📖	mathematical	—	`Subfield` `SetLike.instMembership` `instSetLike` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `instRingSubtypeMem` `DivisionRing.toRing`	—	—
`coe_copy` 📖	mathematical	`SetLike.coe` `Subfield` `instSetLike`	`SetLike.coe` `Subfield` `instSetLike` `copy`	—	—
`coe_div` 📖	mathematical	—	`Subfield` `SetLike.instMembership` `instSetLike` `instDivSubtypeMem` `DivInvMonoid.toDiv` `DivisionRing.toDivInvMonoid`	—	—
`coe_inv` 📖	mathematical	—	`Subfield` `SetLike.instMembership` `instSetLike` `instInvSubtypeMem` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `GroupWithZero.toDivisionMonoid` `DivisionSemiring.toGroupWithZero` `DivisionRing.toDivisionSemiring`	—	—
`coe_mul` 📖	mathematical	—	`Subfield` `SetLike.instMembership` `instSetLike` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `instRingSubtypeMem` `DivisionRing.toRing`	—	—
`coe_neg` 📖	mathematical	—	`Subfield` `SetLike.instMembership` `instSetLike` `NegMemClass.neg` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `DivisionRing.toRing` `SubringClass.toNegMemClass` `Ring.toNonAssocRing` `SubfieldClass.toSubringClass` `instSubfieldClass`	—	`SubringClass.toNegMemClass` `SubfieldClass.toSubringClass` `instSubfieldClass`
`coe_one` 📖	mathematical	—	`Subfield` `SetLike.instMembership` `instSetLike` `OneMemClass.one` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `AddSubmonoidWithOneClass.toOneMemClass` `SubsemiringClass.addSubmonoidWithOneClass` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `SubringClass.toSubsemiringClass` `Ring.toNonAssocRing` `SubfieldClass.toSubringClass` `instSubfieldClass`	—	`AddSubmonoidWithOneClass.toOneMemClass` `SubsemiringClass.addSubmonoidWithOneClass` `SubringClass.toSubsemiringClass` `SubfieldClass.toSubringClass` `instSubfieldClass`
`coe_set_mk` 📖	mathematical	`Set` `Set.instMembership` `Subsemigroup.carrier` `MulOne.toMul` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `NonAssocRing.toNonAssocSemiring` `Ring.toNonAssocRing` `DivisionRing.toRing` `Submonoid.toSubsemigroup` `Subsemiring.toSubmonoid` `Subring.toSubsemiring` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `GroupWithZero.toDivisionMonoid` `DivisionSemiring.toGroupWithZero` `DivisionRing.toDivisionSemiring`	`SetLike.coe` `Subfield` `instSetLike` `Subring` `Ring.toNonAssocRing` `DivisionRing.toRing` `Subring.instSetLike`	—	—
`coe_sub` 📖	mathematical	—	`Subfield` `SetLike.instMembership` `instSetLike` `AddSubgroupClass.sub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `SubringClass.addSubgroupClass` `Ring.toNonAssocRing` `SubfieldClass.toSubringClass` `instSubfieldClass` `SubNegMonoid.toSub`	—	`SubringClass.addSubgroupClass` `SubfieldClass.toSubringClass` `instSubfieldClass`
`coe_subtype` 📖	mathematical	—	`DFunLike.coe` `RingHom` `Subfield` `SetLike.instMembership` `instSetLike` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `toDivisionRing` `RingHom.instFunLike` `subtype`	—	—
`coe_toAddSubgroup` 📖	mathematical	—	`SetLike.coe` `AddSubgroup` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `AddSubgroup.instSetLike` `toAddSubgroup` `Subfield` `instSetLike`	—	—
`coe_toSubmonoid` 📖	mathematical	—	`SetLike.coe` `Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `NonAssocRing.toNonAssocSemiring` `Ring.toNonAssocRing` `DivisionRing.toRing` `Submonoid.instSetLike` `Subsemiring.toSubmonoid` `Subring.toSubsemiring` `toSubring` `Subfield` `instSetLike`	—	—
`coe_toSubring` 📖	mathematical	—	`SetLike.coe` `Subring` `Ring.toNonAssocRing` `DivisionRing.toRing` `Subring.instSetLike` `toSubring` `Subfield` `instSetLike`	—	—
`coe_zero` 📖	mathematical	—	`Subfield` `SetLike.instMembership` `instSetLike` `ZeroMemClass.zero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `DivisionRing.toRing` `AddSubmonoidClass.toZeroMemClass` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `AddSubgroupClass.toAddSubmonoidClass` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `SubringClass.addSubgroupClass` `SubfieldClass.toSubringClass` `instSubfieldClass`	—	`AddSubmonoidClass.toZeroMemClass` `AddSubgroupClass.toAddSubmonoidClass` `SubringClass.addSubgroupClass` `SubfieldClass.toSubringClass` `instSubfieldClass`
`copy_eq` 📖	mathematical	`SetLike.coe` `Subfield` `instSetLike`	`copy`	—	`SetLike.coe_injective`
`div_mem` 📖	mathematical	`Subfield` `SetLike.instMembership` `instSetLike`	`Subfield` `SetLike.instMembership` `instSetLike` `DivInvMonoid.toDiv` `DivisionRing.toDivInvMonoid`	—	`div_mem` `SubfieldClass.toSubgroupClass` `instSubfieldClass`
`ext` 📖	—	`Subfield` `SetLike.instMembership` `instSetLike`	—	—	`SetLike.ext`
`ext_iff` 📖	mathematical	—	`Subfield` `SetLike.instMembership` `instSetLike`	—	`ext`
`instSubfieldClass` 📖	mathematical	—	`SubfieldClass` `Subfield` `instSetLike`	—	`Subsemigroup.mul_mem'` `Submonoid.one_mem'` `Subsemiring.add_mem'` `Subsemiring.zero_mem'` `Subring.neg_mem'` `inv_mem'`
`intCast_mem` 📖	mathematical	—	`Subfield` `SetLike.instMembership` `instSetLike` `AddGroupWithOne.toIntCast` `Ring.toAddGroupWithOne` `DivisionRing.toRing`	—	`intCast_mem` `SubfieldClass.toSubringClass` `instSubfieldClass`
`inv_mem` 📖	mathematical	`Subfield` `SetLike.instMembership` `instSetLike`	`Subfield` `SetLike.instMembership` `instSetLike` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `GroupWithZero.toDivisionMonoid` `DivisionSemiring.toGroupWithZero` `DivisionRing.toDivisionSemiring`	—	`InvMemClass.inv_mem` `SubfieldClass.toInvMemClass` `instSubfieldClass`
`inv_mem'` 📖	mathematical	`Set` `Set.instMembership` `Subsemigroup.carrier` `MulOne.toMul` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `NonAssocRing.toNonAssocSemiring` `Ring.toNonAssocRing` `DivisionRing.toRing` `Submonoid.toSubsemigroup` `Subsemiring.toSubmonoid` `Subring.toSubsemiring` `toSubring`	`Set` `Set.instMembership` `Subsemigroup.carrier` `MulOne.toMul` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `NonAssocRing.toNonAssocSemiring` `Ring.toNonAssocRing` `DivisionRing.toRing` `Submonoid.toSubsemigroup` `Subsemiring.toSubmonoid` `Subring.toSubsemiring` `toSubring` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `GroupWithZero.toDivisionMonoid` `DivisionSemiring.toGroupWithZero` `DivisionRing.toDivisionSemiring`	—	—
`mem_carrier` 📖	mathematical	—	`Set` `Set.instMembership` `Subsemigroup.carrier` `MulOne.toMul` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `NonAssocRing.toNonAssocSemiring` `Ring.toNonAssocRing` `DivisionRing.toRing` `Submonoid.toSubsemigroup` `Subsemiring.toSubmonoid` `Subring.toSubsemiring` `toSubring` `Subfield` `SetLike.instMembership` `instSetLike`	—	—
`mem_mk` 📖	mathematical	`Set` `Set.instMembership` `Subsemigroup.carrier` `MulOne.toMul` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `NonAssocRing.toNonAssocSemiring` `Ring.toNonAssocRing` `DivisionRing.toRing` `Submonoid.toSubsemigroup` `Subsemiring.toSubmonoid` `Subring.toSubsemiring` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `GroupWithZero.toDivisionMonoid` `DivisionSemiring.toGroupWithZero` `DivisionRing.toDivisionSemiring`	`Subfield` `SetLike.instMembership` `instSetLike` `Subring` `Ring.toNonAssocRing` `DivisionRing.toRing` `Subring.instSetLike`	—	—
`mem_toAddSubgroup` 📖	mathematical	—	`AddSubgroup` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `SetLike.instMembership` `AddSubgroup.instSetLike` `toAddSubgroup` `Subfield` `instSetLike`	—	—
`mem_toSubmonoid` 📖	mathematical	—	`Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `NonAssocRing.toNonAssocSemiring` `Ring.toNonAssocRing` `DivisionRing.toRing` `SetLike.instMembership` `Submonoid.instSetLike` `Subsemiring.toSubmonoid` `Subring.toSubsemiring` `toSubring` `Subfield` `instSetLike`	—	—
`mem_toSubring` 📖	mathematical	—	`Subring` `Ring.toNonAssocRing` `DivisionRing.toRing` `SetLike.instMembership` `Subring.instSetLike` `toSubring` `Subfield` `instSetLike`	—	—
`mk_le_mk` 📖	mathematical	`Set` `Set.instMembership` `Subsemigroup.carrier` `MulOne.toMul` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `NonAssocRing.toNonAssocSemiring` `Ring.toNonAssocRing` `DivisionRing.toRing` `Submonoid.toSubsemigroup` `Subsemiring.toSubmonoid` `Subring.toSubsemiring` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `GroupWithZero.toDivisionMonoid` `DivisionSemiring.toGroupWithZero` `DivisionRing.toDivisionSemiring`	`Subfield` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `Subring` `Ring.toNonAssocRing` `DivisionRing.toRing` `Subring.instPartialOrder`	—	—
`mul_mem` 📖	mathematical	`Subfield` `SetLike.instMembership` `instSetLike`	`Subfield` `SetLike.instMembership` `instSetLike` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `DivisionRing.toRing`	—	`MulMemClass.mul_mem` `SubmonoidClass.toMulMemClass` `SubgroupClass.toSubmonoidClass` `SubfieldClass.toSubgroupClass` `instSubfieldClass`
`neg_mem` 📖	mathematical	`Subfield` `SetLike.instMembership` `instSetLike`	`Subfield` `SetLike.instMembership` `instSetLike` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `DivisionRing.toRing`	—	`NegMemClass.neg_mem` `SubringClass.toNegMemClass` `SubfieldClass.toSubringClass` `instSubfieldClass`
`one_mem` 📖	mathematical	—	`Subfield` `SetLike.instMembership` `instSetLike` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing`	—	`OneMemClass.one_mem` `AddSubmonoidWithOneClass.toOneMemClass` `SubsemiringClass.addSubmonoidWithOneClass` `SubringClass.toSubsemiringClass` `SubfieldClass.toSubringClass` `instSubfieldClass`
`pow_mem` 📖	mathematical	`Subfield` `SetLike.instMembership` `instSetLike`	`Subfield` `SetLike.instMembership` `instSetLike` `Monoid.toPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring`	—	`pow_mem` `SubgroupClass.toSubmonoidClass` `SubfieldClass.toSubgroupClass` `instSubfieldClass`
`sub_mem` 📖	mathematical	`Subfield` `SetLike.instMembership` `instSetLike`	`Subfield` `SetLike.instMembership` `instSetLike` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `DivisionRing.toRing`	—	`sub_mem` `SubringClass.addSubgroupClass` `SubfieldClass.toSubringClass` `instSubfieldClass`
`subtype_apply` 📖	mathematical	—	`DFunLike.coe` `RingHom` `Subfield` `SetLike.instMembership` `instSetLike` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `toDivisionRing` `RingHom.instFunLike` `subtype`	—	—
`subtype_injective` 📖	mathematical	—	`Subfield` `SetLike.instMembership` `instSetLike` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `toDivisionRing` `RingHom.instFunLike` `subtype`	—	`Subtype.coe_injective`
`toSubring_subtype_eq_subtype` 📖	mathematical	—	`Subring.subtype` `Ring.toNonAssocRing` `DivisionRing.toRing` `toSubring` `subtype`	—	`Subring.instSubringClass`
`zero_mem` 📖	mathematical	—	`Subfield` `SetLike.instMembership` `instSetLike` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `DivisionRing.toRing`	—	`ZeroMemClass.zero_mem` `AddSubmonoidClass.toZeroMemClass` `AddSubgroupClass.toAddSubmonoidClass` `SubringClass.addSubgroupClass` `SubfieldClass.toSubringClass` `instSubfieldClass`
`zpow_mem` 📖	mathematical	`Subfield` `SetLike.instMembership` `instSetLike`	`Subfield` `SetLike.instMembership` `instSetLike` `DivInvMonoid.toZPow` `DivisionRing.toDivInvMonoid`	—	`zpow_mem` `SubfieldClass.toSubgroupClass` `instSubfieldClass`
`zsmul_mem` 📖	mathematical	`Subfield` `SetLike.instMembership` `instSetLike`	`Subfield` `SetLike.instMembership` `instSetLike` `SubNegMonoid.toZSMul` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `DivisionRing.toRing`	—	`zsmul_mem` `SubringClass.addSubgroupClass` `SubfieldClass.toSubringClass` `instSubfieldClass`

SubfieldClass

Definitions

Name	Category	Theorems
`instNNRatCast` 📖	CompOp	1 math math: `coe_nnratCast`
`instRatCast` 📖	CompOp	1 math math: `coe_ratCast`
`instSMulNNRat` 📖	CompOp	1 math math: `coe_nnqsmul`
`instSMulRat` 📖	CompOp	1 math math: `coe_qsmul`
`toDivisionRing` 📖	CompOp	—
`toField` 📖	CompOp	3 math math: `IntermediateField.coe_add`, `IntermediateField.coe_mul`, `toIntermediateField'_toSubalgebra`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_nnqsmul` 📖	mathematical	—	`SetLike.instMembership` `NNRat` `instSMulNNRat` `NNRat.smulDivisionSemiring` `DivisionRing.toDivisionSemiring`	—	—
`coe_nnratCast` 📖	mathematical	—	`SetLike.instMembership` `NNRat.cast` `instNNRatCast` `DivisionRing.toNNRatCast`	—	—
`coe_qsmul` 📖	mathematical	—	`SetLike.instMembership` `instSMulRat` `Rat.smulDivisionRing`	—	—
`coe_ratCast` 📖	mathematical	—	`SetLike.instMembership` `instRatCast` `DivisionRing.toRatCast`	—	—
`nnqsmul_mem` 📖	mathematical	`SetLike.instMembership`	`SetLike.instMembership` `NNRat` `NNRat.smulDivisionSemiring` `DivisionRing.toDivisionSemiring`	—	`NNRat.smul_def` `MulMemClass.mul_mem` `SubmonoidClass.toMulMemClass` `SubgroupClass.toSubmonoidClass` `toSubgroupClass` `nnratCast_mem`
`nnratCast_mem` 📖	mathematical	—	`SetLike.instMembership` `NNRat.cast` `DivisionRing.toNNRatCast`	—	`NNRat.cast_def` `div_mem` `toSubgroupClass` `natCast_mem` `SubsemiringClass.addSubmonoidWithOneClass` `SubringClass.toSubsemiringClass` `toSubringClass`
`ofScientific_mem` 📖	mathematical	—	`SetLike.instMembership` `NNRatCast.toOfScientific` `DivisionRing.toNNRatCast`	—	`nnratCast_mem`
`qsmul_mem` 📖	mathematical	`SetLike.instMembership`	`SetLike.instMembership` `Rat.smulDivisionRing`	—	`Rat.smul_def` `MulMemClass.mul_mem` `SubmonoidClass.toMulMemClass` `SubgroupClass.toSubmonoidClass` `toSubgroupClass` `ratCast_mem`
`ratCast_mem` 📖	mathematical	—	`SetLike.instMembership` `DivisionRing.toRatCast`	—	`Rat.cast_def` `div_mem` `toSubgroupClass` `intCast_mem` `toSubringClass` `natCast_mem` `SubsemiringClass.addSubmonoidWithOneClass` `SubringClass.toSubsemiringClass`
`toInvMemClass` 📖	mathematical	—	`InvMemClass` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `GroupWithZero.toDivisionMonoid` `DivisionSemiring.toGroupWithZero` `DivisionRing.toDivisionSemiring`	—	—
`toSubgroupClass` 📖	mathematical	—	`SubgroupClass` `DivisionRing.toDivInvMonoid`	—	`SubsemiringClass.toSubmonoidClass` `SubringClass.toSubsemiringClass` `toSubringClass` `toInvMemClass`
`toSubringClass` 📖	mathematical	—	`SubringClass` `Ring.toNonAssocRing` `DivisionRing.toRing`	—	—

Subring

Definitions

Name	Category	Theorems
`toSubfield` 📖	CompOp	—

(root)

Definitions

Name	Category	Theorems
`SubfieldClass` 📖	CompData	2 math math: `Subfield.instSubfieldClass`, `IntermediateField.instSubfieldClass`

---

← Back to Index