Documentation Verification Report

Subfield

📁 Source: Mathlib/SetTheory/Cardinal/Subfield.lean

Statistics

Metric	Count
Definitions `Subfield`	1
Theorems `cardinalMk_closure`, `cardinalMk_closure_le_max`	2
Total	3

Subfield

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cardinalMk_closure` 📖	mathematical	—	`Subfield` `SetLike.instMembership` `instSetLike` `closure` `Set.Elem`	—	`LE.le.antisymm` `LE.le.trans_eq` `cardinalMk_closure_le_max` `max_eq_left` `Cardinal.mk_le_mk_of_subset` `subset_closure`
`cardinalMk_closure_le_max` 📖	mathematical	—	`Cardinal` `Cardinal.instLE` `Subfield` `SetLike.instMembership` `instSetLike` `closure` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `Cardinal.instConditionallyCompleteLinearOrderBot` `Set.Elem` `Cardinal.aleph0`	—	`LE.le.trans` `Cardinal.mk_le_of_surjective` `Cardinal.lift_uzero` `Cardinal.mk_sum` `Cardinal.lift_lt_aleph0` `Cardinal.lt_aleph0_of_finite` `Finite.of_fintype` `lt_or_ge` `max_eq_right` `LT.lt.le` `Cardinal.add_lt_aleph0` `max_eq_left` `Cardinal.add_eq_right` `WType.cardinalMk_le_max_aleph0_of_finite'` `Fintype.complete` `Bool.instFinite`

(root)

Definitions

Name	Category	Theorems
`Subfield` 📖	CompData	255 math math: `Subfield.ext_iff`, `FixedPoints.instFiniteDimensionalSubtypeMemSubfieldSubfield`, `Polynomial.Splits.mem_subfield_of_isRoot`, `Subfield.rank_comap`, `IntermediateField.fieldRange_le`, `FixedPoints.finrank_eq_card`, `IntermediateField.sSup_toSubfield`, `Subfield.map_inf`, `FixedPoints.minpoly.monic`, `HahnSeries.mem_cardSuppLTSubfield`, `FixedPoints.minpoly.irreducible`, `Subfield.mem_sSup_of_directedOn`, `Subfield.add_mem`, `Subfield.mem_sInf`, `NumberField.IsCMField.isConj_complexConj`, `Subfield.inf_relrank_left`, `NumberField.IsCMField.zpowers_complexConj_eq_top`, `Subfield.coe_add`, `NumberField.instIsTotallyRealSubtypeMemSubfieldOfIsAlgebraic`, `Subfield.zsmul_mem`, `Subfield.relfinrank_eq_one_iff`, `Subfield.closure_le`, `Subfield.mem_toSubring`, `FixedPoints.isSeparable`, `NumberField.IsCMField.equivInfinitePlace_symm_apply`, `NumberField.IsCMField.units_rank_eq_units_rank`, `NumberField.mem_maximalRealSubfield_iff`, `Subfield.multiset_prod_mem`, `NumberField.CMExtension.algebraMap_equivMaximalRealSubfield_symm_apply`, `FixedPoints.minpoly.eval₂'`, `Subfield.mem_top`, `Subfield.relfinrank_mul_finrank_top`, `RingHom.mem_fieldRange_self`, `Subfield.extendScalars_toSubfield`, `Subfield.relfinrank_eq_finrank_of_le`, `Subfield.relfinrank_mul_relfinrank_eq_inf_relfinrank`, `Subfield.relfinrank_top_left`, `Subfield.relfinrank_inf_mul_relfinrank_of_le`, `Subfield.coe_top`, `Subfield.map_sup`, `Subfield.coe_iSup_of_directed`, `Subfield.splits_bot`, `Subfield.coe_mul`, `Subfield.map_iInf`, `Subfield.cardinalMk_closure_le_max`, `NumberField.isTotallyReal_sup`, `Subfield.mem_closure`, `FixedPoints.rank_le_card`, `Subfield.coe_toIntermediateField`, `NumberField.isTotallyReal_top_iff`, `instSubsingletonSubfieldRat`, `Subfield.mk_le_mk`, `Subfield.relrank_mul_rank_top`, `IntermediateField.subset_adjoin_of_subset_left`, `Subfield.relrank_top_left`, `Subfield.closure_iUnion`, `NumberField.IsCMField.isQuadraticExtension`, `Subfield.instSubfieldClass`, `RingHom.eqOn_field_closure`, `NumberField.IsCMField.orderOf_complexConj`, `IntermediateField.iInf_toSubfield`, `Subfield.mem_bot_iff_pow_eq_self`, `Subfield.coe_inv`, `Subfield.isTotallyReal_bot`, `NumberField.IsCMField.regulator_div_regulator_eq_two_pow_mul_indexRealUnits_inv`, `Subfield.list_prod_mem`, `Subfield.coe_zero`, `Subfield.mem_closure_iff`, `IntermediateField.coe_type_toSubfield`, `Subfield.smulCommClass_left`, `FixedPoints.instSMulCommClassSubtypeMemSubfieldSubfield`, `RingHom.coe_rangeRestrictField`, `Subfield.closure_mono`, `Subfield.extendScalars_le_extendScalars_iff`, `FixedPoints.normal`, `Subfield.extendScalars_inf`, `Subfield.finrank_comap`, `Subfield.mem_inf`, `NumberField.instIsTotallyRealSubtypeMemSubfieldTop`, `FixedPoints.finrank_le_card`, `Subfield.smul_def`, `Subfield.mem_iInf`, `HahnSeries.cardSuppLTSubfield_carrier`, `Subfield.relfinrank_comap_comap_eq_relfinrank_inf`, `Subfield.sum_mem`, `NumberField.IsCMField.complexConj_apply_apply`, `Subfield.mem_closure_of_mem`, `NumberField.of_subfield`, `Subfield.zpow_mem`, `NumberField.IsCMField.coe_ringOfIntegersComplexConj`, `Subfield.relrank_comap_comap_eq_relrank_inf`, `Subfield.prod_mem`, `NumberField.IsCMField.equivInfinitePlace_apply`, `IntermediateField.mem_toSubfield`, `NumberField.IsCMField.is_quadratic`, `NumberField.isTotallyReal_iSup`, `NumberField.IsCMField.complexConj_apply_eq_self`, `Subfield.algebraMap_ofSubfield`, `Subfield.map_comap_eq`, `Subfield.zero_mem`, `Subfield.coe_iInf`, `Subfield.bot_eq_of_zMod_algebra`, `Subfield.map_bot`, `Subfield.gc_map_comap`, `NumberField.IsCMField.complexEmbedding_complexConj`, `Subfield.coe_comap`, `IsFractionRing.closure_range_algebraMap`, `Subfield.topologicalClosure_minimal`, `Subfield.sub_mem`, `Subfield.extendScalars.orderIso_symm_apply`, `FixedPoints.minpoly.irreducible_aux`, `NumberField.CMExtension.equivMaximalRealSubfield_apply`, `NumberField.isTotallyReal_iff_le_maximalRealSubfield`, `Subfield.subtype_apply`, `Subfield.roots_X_pow_char_sub_X_bot`, `Subfield.inf_relfinrank_left`, `Subfield.relfinrank_top_right`, `NumberField.maximalRealSubfield_eq_top_iff_isTotallyReal`, `NumberField.IsCMField.card_infinitePlace_eq_card_infinitePlace`, `Subfield.relfinrank_inf_mul_relfinrank`, `instSubsingletonSubfieldZMod`, `Subfield.coe_one`, `Subfield.smulCommClass_right`, `Subfield.instFaithfulSMulSubtypeMem`, `Subfield.extendScalars_top`, `IntermediateField.coe_toSubfield`, `Subfield.cardinalMk_closure`, `NumberField.IsTotallyReal.maximalRealSubfield_eq_top`, `Subfield.coe_set_mk`, `Subfield.continuousSMul`, `Subfield.neg_mem`, `Subfield.closure_sUnion`, `Subfield.fieldRange_subtype`, `Subfield.coe_subtype`, `Subfield.multiset_sum_mem`, `Subfield.relrank_mul_relrank_eq_inf_relrank`, `Subfield.pow_mem`, `Subfield.bot_eq_of_charZero`, `Subfield.mem_iSup_of_directed`, `NumberField.isTotallyReal_maximalRealSubfield`, `Subfield.relrank_inf_mul_relrank`, `Subfield.comap_top`, `Subfield.one_mem`, `Subfield.coe_inf`, `Subfield.sInf_toSubring`, `Subfield.inv_mem`, `Subfield.list_sum_mem`, `Subfield.inf_relfinrank_right`, `Subfield.le_extendScalars_iff`, `Subfield.map_iSup`, `FixedPoints.toAlgAut_surjective`, `Subfield.relrank_inf_mul_relrank_of_le`, `Subfield.relrank_dvd_rank_top_of_le`, `FixedPoints.isIntegral`, `RingHom.coe_fieldRange`, `RingHom.rangeRestrictFieldEquiv_apply_symm_apply`, `Subfield.mem_toAddSubgroup`, `Subfield.mem_mk`, `FixedPoints.smul_polynomial`, `NumberField.IsCMField.ringOfIntegersComplexConj_eq_self_iff`, `Subfield.extendScalars_le_iff`, `NumberField.IsCMField.mem_realUnits_iff`, `IntermediateField.iSup_toSubfield`, `Subfield.charP`, `RingHom.fieldRange_eq_map`, `Subfield.coe_sInf`, `Subfield.extendScalars.orderIso_apply`, `Subfield.map_le_iff_le_comap`, `Subfield.relrank_top_right`, `Subfield.coe_toSubring`, `Subfield.relrank_eq_rank_of_le`, `RingHom.rangeRestrictField_bijective`, `Subfield.closure_preimage_le`, `Complex.uniformContinuous_ringHom_eq_id_or_conj`, `NumberField.IsCMField.exists_isConj`, `Subfield.map_mem_map`, `FixedPoints.toAlgHom_bijective`, `Subfield.coe_copy`, `mem_bot_iff_intCast`, `Subfield.isClosed_topologicalClosure`, `IsGaloisGroup.fixedPoints`, `Matrix.mem_subfield_of_mul_eq_one_of_mem_subfield_right`, `IntermediateField.top_toSubfield`, `ZMod.instSubsingletonSubfield`, `Subfield.coe_sSup_of_directedOn`, `Subfield.extendScalars_sup`, `Subfield.relfinrank_dvd_finrank_top_of_le`, `Subfield.mul_mem`, `Subfield.closure_eq`, `NumberField.IsCMField.complexConj_eq_self_iff`, `Subfield.expChar`, `Subfield.mem_toSubmonoid`, `Subfield.instIsScalarTowerSubtypeMem`, `IntermediateField.adjoin_le_subfield`, `Subfield.closure_union`, `IntermediateField.sInf_toSubfield`, `NumberField.IsTotallyReal.le_maximalRealSubfield`, `Subfield.lift_rank_comap`, `Subfield.comap_iInf`, `Subfield.div_mem`, `Subfield.relrank_eq_one_iff`, `FixedPoints.minpoly_eq_minpoly`, `Complex.subfield_eq_of_closed`, `NumberField.IsCMField.RingOfIntegers.complexConj_eq_self_iff`, `RingHom.mem_fieldRange`, `Subfield.closure_empty`, `IntermediateField.inf_toSubfield`, `Subfield.coe_div`, `Subfield.subset_closure`, `Subfield.coe_toAddSubgroup`, `RingHom.fieldRange_eq_top_iff`, `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`, `Subfield.card_bot`, `IntermediateField.sup_toSubfield`, `Subfield.mem_map`, `RingHom.rangeRestrictFieldEquiv_apply_coe`, `Subfield.coe_map`, `Subfield.extendScalars_self`, `Subfield.intCast_mem`, `Subfield.mem_extendScalars`, `ZMod.fieldRange_castHom_eq_bot`, `RingHom.field_closure_preimage_le`, `Real.subfield_eq_of_closed`, `Subfield.closure_univ`, `Subfield.lift_relrank_comap_comap_eq_lift_relrank_inf`, `IntermediateField.toSubfield_injective`, `Subfield.subtype_injective`, `Subfield.completableTopField`, `Subfield.coe_sub`, `Subfield.inf_relrank_right`, `NumberField.instIsAlgebraicSubtypeMemSubfield`, `NumberField.IsCMField.complexConj_torsion`, `Subfield.isGLB_sInf`, `Subfield.mem_carrier`, `Subfield.coe_neg`, `Subfield.le_topologicalClosure`, `NumberField.IsCMField.Units.complexConj_eq_self_iff`, `Subfield.toIsStrictOrderedRing`, `Subfield.coe_toSubmonoid`, `Subfield.coe_extendScalars`, `Subfield.extendScalars_injective`, `NumberField.IsCMField.regOfFamily_realFunSystem`, `FixedPoints.minpoly.of_eval₂`, `Subfield.mem_comap`, `FixedBy.subfield_mem_iff`, `Subfield.comap_inf`, `IntermediateField.adjoin_contains_field_as_subfield`

---

← Back to Index