Basic

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

Statistics

Metric	Count
Definitions `subfieldCongr`, `eqLocusField`, `fieldRange`, `fintypeFieldRange`, `rangeRestrictField`, `rangeRestrictFieldEquiv`, `closure`, `comap`, `gi`, `inclusion`, `instCompleteLattice`, `instDistribMulActionSubtypeMem`, `instInfSet`, `instInhabited`, `instMin`, `instModuleSubtypeMem`, `instMulActionSubtypeMem`, `instMulActionWithZeroSubtypeMem`, `instMulDistribMulActionSubtypeMem`, `instMulSemiringActionSubtypeMem`, `instSMulSubtypeMem`, `instSMulWithZeroSubtypeMem`, `instTop`, `map`, `toAlgebra`, `topEquiv`	26
Theorems `coe_fieldRange`, `coe_rangeRestrictField`, `eqOn_field_closure`, `eq_of_eqOn_of_field_closure_eq_top`, `eq_of_eqOn_subfield_top`, `fieldRange_eq_map`, `fieldRange_eq_top_iff`, `field_closure_preimage_le`, `map_fieldRange`, `map_field_closure`, `mem_eqLocusField`, `mem_fieldRange`, `mem_fieldRange_self`, `rangeRestrictFieldEquiv_apply_coe`, `rangeRestrictFieldEquiv_apply_symm_apply`, `rangeRestrictField_bijective`, `algebraMap_ofSubfield`, `closure_empty`, `closure_eq`, `closure_eq_of_le`, `closure_iUnion`, `closure_induction`, `closure_le`, `closure_mono`, `closure_preimage_le`, `closure_sUnion`, `closure_union`, `closure_univ`, `coe_comap`, `coe_iInf`, `coe_iSup_of_directed`, `coe_inf`, `coe_map`, `coe_sInf`, `coe_sSup_of_directedOn`, `coe_top`, `comap_comap`, `comap_iInf`, `comap_inf`, `comap_map`, `comap_top`, `fieldRange_subtype`, `gc_map_comap`, `instFaithfulSMulSubtypeMem`, `instIsScalarTowerSubtypeMem`, `isGLB_sInf`, `list_prod_mem`, `list_sum_mem`, `map_bot`, `map_comap_eq`, `map_comap_eq_self`, `map_comap_eq_self_of_surjective`, `map_iInf`, `map_iSup`, `map_inf`, `map_le_iff_le_comap`, `map_map`, `map_sup`, `mem_closure`, `mem_closure_iff`, `mem_closure_of_mem`, `mem_comap`, `mem_iInf`, `mem_iSup_of_directed`, `mem_inf`, `mem_map`, `mem_sInf`, `mem_sSup_of_directedOn`, `mem_top`, `multiset_prod_mem`, `multiset_sum_mem`, `notMem_of_notMem_closure`, `prod_mem`, `sInf_toSubring`, `smulCommClass_left`, `smulCommClass_right`, `smul_def`, `subring_closure_le`, `subset_closure`, `sum_mem`	80
Total	106

RingEquiv

Definitions

Name	Category	Theorems
`subfieldCongr` 📖	CompOp	—

RingHom

Definitions

Name	Category	Theorems
`eqLocusField` 📖	CompOp	1 math math: `mem_eqLocusField`
`fieldRange` 📖	CompOp	29 math math: `Subfield.rank_comap`, `IntermediateField.fieldRange_le`, `mem_fieldRange_self`, `coe_rangeRestrictField`, `Subfield.finrank_comap`, `Subfield.relfinrank_comap_comap_eq_relfinrank_inf`, `Subfield.relrank_comap_comap_eq_relrank_inf`, `map_fieldRange`, `Subfield.map_comap_eq`, `Subfield.bot_eq_of_zMod_algebra`, `AlgHom.fieldRange_toSubfield`, `Subfield.fieldRange_subtype`, `IsFractionRing.ringHom_fieldRange_eq_of_comp_eq_of_range_eq`, `Subfield.bot_eq_of_charZero`, `coe_fieldRange`, `rangeRestrictFieldEquiv_apply_symm_apply`, `IsFractionRing.ringHom_fieldRange_eq_of_comp_eq`, `fieldRange_eq_map`, `rangeRestrictField_bijective`, `IntermediateField.bot_toSubfield`, `IsFractionRing.lift_fieldRange_eq_of_range_eq`, `Subfield.lift_rank_comap`, `Complex.subfield_eq_of_closed`, `mem_fieldRange`, `fieldRange_eq_top_iff`, `IsFractionRing.lift_fieldRange`, `rangeRestrictFieldEquiv_apply_coe`, `ZMod.fieldRange_castHom_eq_bot`, `Subfield.lift_relrank_comap_comap_eq_lift_relrank_inf`
`fintypeFieldRange` 📖	CompOp	—
`rangeRestrictField` 📖	CompOp	2 math math: `coe_rangeRestrictField`, `rangeRestrictField_bijective`
`rangeRestrictFieldEquiv` 📖	CompOp	2 math math: `rangeRestrictFieldEquiv_apply_symm_apply`, `rangeRestrictFieldEquiv_apply_coe`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_fieldRange` 📖	mathematical	—	`SetLike.coe` `Subfield` `Subfield.instSetLike` `fieldRange` `Set.range` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `instFunLike`	—	—
`coe_rangeRestrictField` 📖	mathematical	—	`Subfield` `SetLike.instMembership` `Subfield.instSetLike` `fieldRange` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `Subfield.toDivisionRing` `instFunLike` `rangeRestrictField`	—	—
`eqOn_field_closure` 📖	mathematical	`Set.EqOn` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `instFunLike`	`SetLike.coe` `Subfield` `Subfield.instSetLike` `Subfield.closure`	—	`Subfield.closure_le`
`eq_of_eqOn_of_field_closure_eq_top` 📖	—	`Subfield.closure` `Top.top` `Subfield` `Subfield.instTop` `Set.EqOn` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `instFunLike`	—	—	`eq_of_eqOn_subfield_top` `eqOn_field_closure`
`eq_of_eqOn_subfield_top` 📖	—	`Set.EqOn` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `instFunLike` `SetLike.coe` `Subfield` `Subfield.instSetLike` `Top.top` `Subfield.instTop`	—	—	`ext`
`fieldRange_eq_map` 📖	mathematical	—	`fieldRange` `Subfield.map` `Top.top` `Subfield` `Subfield.instTop`	—	`Subfield.ext`
`fieldRange_eq_top_iff` 📖	mathematical	—	`fieldRange` `Top.top` `Subfield` `Subfield.instTop` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `instFunLike`	—	`SetLike.ext'_iff` `Set.range_eq_univ`
`field_closure_preimage_le` 📖	mathematical	—	`Subfield` `Preorder.toLE` `PartialOrder.toPreorder` `Subfield.instPartialOrder` `Subfield.closure` `Set.preimage` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `instFunLike` `Subfield.comap`	—	`Subfield.closure_le` `SetLike.mem_coe` `Subfield.mem_comap` `Subfield.subset_closure`
`map_fieldRange` 📖	mathematical	—	`Subfield.map` `fieldRange` `comp` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring`	—	`fieldRange_eq_map` `Subfield.map_map`
`map_field_closure` 📖	mathematical	—	`Subfield.map` `Subfield.closure` `Set.image` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `instFunLike`	—	`GaloisConnection.l_comm_of_u_comm` `Set.image_preimage` `Subfield.gc_map_comap` `GaloisInsertion.gc`
`mem_eqLocusField` 📖	mathematical	—	`Subfield` `SetLike.instMembership` `Subfield.instSetLike` `eqLocusField` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `instFunLike`	—	—
`mem_fieldRange` 📖	mathematical	—	`Subfield` `SetLike.instMembership` `Subfield.instSetLike` `fieldRange` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `instFunLike`	—	—
`mem_fieldRange_self` 📖	mathematical	—	`Subfield` `SetLike.instMembership` `Subfield.instSetLike` `fieldRange` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `instFunLike`	—	—
`rangeRestrictFieldEquiv_apply_coe` 📖	mathematical	—	`Subfield` `SetLike.instMembership` `Subfield.instSetLike` `fieldRange` `DFunLike.coe` `RingEquiv` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `DivisionRing.toRing` `Subfield.instRingSubtypeMem` `Distrib.toAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `rangeRestrictFieldEquiv` `RingHom` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `instFunLike`	—	—
`rangeRestrictFieldEquiv_apply_symm_apply` 📖	mathematical	—	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `instFunLike` `RingEquiv` `Subfield` `SetLike.instMembership` `Subfield.instSetLike` `fieldRange` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Subfield.instRingSubtypeMem` `DivisionRing.toRing` `Distrib.toAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `RingEquiv.symm` `rangeRestrictFieldEquiv`	—	`rangeRestrictFieldEquiv_apply_coe` `RingEquiv.apply_symm_apply`
`rangeRestrictField_bijective` 📖	mathematical	—	`Function.Bijective` `Subfield` `SetLike.instMembership` `Subfield.instSetLike` `fieldRange` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `Subfield.toDivisionRing` `instFunLike` `rangeRestrictField`	—	`Equiv.bijective` `injective` `DivisionRing.isSimpleRing` `IsSimpleRing.instNontrivial`

Subfield

Definitions

Name	Category	Theorems
`closure` 📖	CompOp	25 math math: `closure_le`, `cardinalMk_closure_le_max`, `mem_closure`, `closure_iUnion`, `RingHom.eqOn_field_closure`, `mem_closure_iff`, `closure_mono`, `mem_closure_of_mem`, `IsFractionRing.closure_range_algebraMap`, `subring_closure_le`, `cardinalMk_closure`, `closure_sUnion`, `IsFractionRing.ringHom_fieldRange_eq_of_comp_eq_of_range_eq`, `IsFractionRing.ringHom_fieldRange_eq_of_comp_eq`, `closure_preimage_le`, `IsFractionRing.lift_fieldRange_eq_of_range_eq`, `closure_eq`, `closure_union`, `RingHom.map_field_closure`, `closure_empty`, `subset_closure`, `IsFractionRing.lift_fieldRange`, `IntermediateField.adjoin_toSubfield`, `RingHom.field_closure_preimage_le`, `closure_univ`
`comap` 📖	CompOp	29 math math: `rank_comap`, `comap_comap`, `relrank_comap_comap_eq_relrank_of_surjective`, `lift_relrank_comap_comap_eq_lift_relrank_of_surjective`, `relfinrank_comap_comap_eq_relfinrank_of_le`, `finrank_comap`, `relfinrank_comap_comap_eq_relfinrank_inf`, `relrank_comap`, `relrank_comap_comap_eq_relrank_inf`, `lift_relrank_comap_comap_eq_lift_relrank_of_le`, `map_comap_eq`, `gc_map_comap`, `coe_comap`, `map_comap_eq_self`, `map_comap_eq_self_of_surjective`, `relrank_comap_comap_eq_relrank_of_le`, `comap_top`, `lift_relrank_comap`, `relfinrank_comap`, `map_le_iff_le_comap`, `closure_preimage_le`, `comap_map`, `lift_rank_comap`, `comap_iInf`, `relfinrank_comap_comap_eq_relfinrank_of_surjective`, `RingHom.field_closure_preimage_le`, `lift_relrank_comap_comap_eq_lift_relrank_inf`, `mem_comap`, `comap_inf`
`gi` 📖	CompOp	—
`inclusion` 📖	CompOp	—
`instCompleteLattice` 📖	CompOp	28 math math: `IntermediateField.sSup_toSubfield`, `mem_sSup_of_directedOn`, `map_sup`, `coe_iSup_of_directed`, `splits_bot`, `NumberField.isTotallyReal_sup`, `closure_iUnion`, `mem_bot_iff_pow_eq_self`, `isTotallyReal_bot`, `extendScalars_inf`, `NumberField.isTotallyReal_iSup`, `bot_eq_of_zMod_algebra`, `map_bot`, `roots_X_pow_char_sub_X_bot`, `extendScalars_top`, `closure_sUnion`, `bot_eq_of_charZero`, `mem_iSup_of_directed`, `map_iSup`, `IntermediateField.iSup_toSubfield`, `mem_bot_iff_intCast`, `coe_sSup_of_directedOn`, `extendScalars_sup`, `closure_union`, `closure_empty`, `card_bot`, `IntermediateField.sup_toSubfield`, `ZMod.fieldRange_castHom_eq_bot`
`instDistribMulActionSubtypeMem` 📖	CompOp	—
`instInfSet` 📖	CompOp	10 math math: `mem_sInf`, `map_iInf`, `IntermediateField.iInf_toSubfield`, `mem_iInf`, `coe_iInf`, `sInf_toSubring`, `coe_sInf`, `IntermediateField.sInf_toSubfield`, `comap_iInf`, `isGLB_sInf`
`instInhabited` 📖	CompOp	—
`instMin` 📖	CompOp	19 math math: `map_inf`, `inf_relrank_left`, `relfinrank_mul_relfinrank_eq_inf_relfinrank`, `relfinrank_inf_mul_relfinrank_of_le`, `mem_inf`, `relfinrank_comap_comap_eq_relfinrank_inf`, `relrank_comap_comap_eq_relrank_inf`, `map_comap_eq`, `inf_relfinrank_left`, `relfinrank_inf_mul_relfinrank`, `relrank_mul_relrank_eq_inf_relrank`, `relrank_inf_mul_relrank`, `coe_inf`, `inf_relfinrank_right`, `relrank_inf_mul_relrank_of_le`, `IntermediateField.inf_toSubfield`, `lift_relrank_comap_comap_eq_lift_relrank_inf`, `inf_relrank_right`, `comap_inf`
`instModuleSubtypeMem` 📖	CompOp	15 math math: `FixedPoints.instFiniteDimensionalSubtypeMemSubfieldSubfield`, `rank_comap`, `FixedPoints.finrank_eq_card`, `relfinrank_mul_finrank_top`, `relfinrank_eq_finrank_of_le`, `FixedPoints.rank_le_card`, `relrank_mul_rank_top`, `finrank_comap`, `FixedPoints.finrank_le_card`, `relfinrank_top_right`, `relrank_dvd_rank_top_of_le`, `relrank_top_right`, `relrank_eq_rank_of_le`, `relfinrank_dvd_finrank_top_of_le`, `lift_rank_comap`
`instMulActionSubtypeMem` 📖	CompOp	2 math math: `relfinrank_eq_finrank_of_le`, `relrank_eq_rank_of_le`
`instMulActionWithZeroSubtypeMem` 📖	CompOp	—
`instMulDistribMulActionSubtypeMem` 📖	CompOp	—
`instMulSemiringActionSubtypeMem` 📖	CompOp	—
`instSMulSubtypeMem` 📖	CompOp	7 math math: `smulCommClass_left`, `FixedPoints.instSMulCommClassSubtypeMemSubfieldSubfield`, `smul_def`, `smulCommClass_right`, `instFaithfulSMulSubtypeMem`, `instIsScalarTowerSubtypeMem`, `FixedPoints.smulCommClass'`
`instSMulWithZeroSubtypeMem` 📖	CompOp	—
`instTop` 📖	CompOp	18 math math: `mem_top`, `relfinrank_top_left`, `coe_top`, `NumberField.isTotallyReal_top_iff`, `relrank_top_left`, `NumberField.instIsTotallyRealSubtypeMemSubfieldTop`, `IsFractionRing.closure_range_algebraMap`, `relfinrank_top_right`, `NumberField.maximalRealSubfield_eq_top_iff_isTotallyReal`, `NumberField.IsTotallyReal.maximalRealSubfield_eq_top`, `comap_top`, `RingHom.fieldRange_eq_map`, `relrank_top_right`, `IntermediateField.top_toSubfield`, `Complex.subfield_eq_of_closed`, `RingHom.fieldRange_eq_top_iff`, `Real.subfield_eq_of_closed`, `closure_univ`
`map` 📖	CompOp	24 math math: `map_inf`, `map_sup`, `map_iInf`, `lift_relrank_map_map`, `relrank_comap`, `IntermediateField.toSubfield_map`, `RingHom.map_fieldRange`, `map_comap_eq`, `map_bot`, `gc_map_comap`, `map_comap_eq_self`, `map_comap_eq_self_of_surjective`, `relrank_map_map`, `map_iSup`, `map_map`, `lift_relrank_comap`, `relfinrank_comap`, `RingHom.fieldRange_eq_map`, `map_le_iff_le_comap`, `comap_map`, `relfinrank_map_map`, `RingHom.map_field_closure`, `mem_map`, `coe_map`
`toAlgebra` 📖	CompOp	39 math math: `NumberField.IsCMField.isConj_complexConj`, `NumberField.IsCMField.zpowers_complexConj_eq_top`, `NumberField.IsCMField.equivInfinitePlace_symm_apply`, `NumberField.CMExtension.algebraMap_equivMaximalRealSubfield_symm_apply`, `extendScalars_toSubfield`, `relfinrank_eq_finrank_of_le`, `IntermediateField.subset_adjoin_of_subset_left`, `NumberField.IsCMField.isQuadraticExtension`, `NumberField.IsCMField.orderOf_complexConj`, `extendScalars_le_extendScalars_iff`, `extendScalars_inf`, `NumberField.IsCMField.complexConj_apply_apply`, `NumberField.IsCMField.coe_ringOfIntegersComplexConj`, `NumberField.IsCMField.equivInfinitePlace_apply`, `NumberField.IsCMField.is_quadratic`, `NumberField.IsCMField.complexConj_apply_eq_self`, `algebraMap_ofSubfield`, `NumberField.IsCMField.complexEmbedding_complexConj`, `extendScalars_top`, `le_extendScalars_iff`, `NumberField.IsCMField.ringOfIntegersComplexConj_eq_self_iff`, `extendScalars_le_iff`, `NumberField.IsCMField.mem_realUnits_iff`, `extendScalars.orderIso_apply`, `relrank_eq_rank_of_le`, `NumberField.IsCMField.exists_isConj`, `extendScalars_sup`, `NumberField.IsCMField.complexConj_eq_self_iff`, `NumberField.IsCMField.RingOfIntegers.complexConj_eq_self_iff`, `NumberField.IsCMField.infinitePlace_complexConj`, `extendScalars.orderIso_symm_apply_coe`, `extendScalars_self`, `mem_extendScalars`, `NumberField.instIsAlgebraicSubtypeMemSubfield`, `NumberField.IsCMField.complexConj_torsion`, `NumberField.IsCMField.Units.complexConj_eq_self_iff`, `coe_extendScalars`, `extendScalars_injective`, `IntermediateField.adjoin_contains_field_as_subfield`
`topEquiv` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`algebraMap_ofSubfield` 📖	mathematical	—	`algebraMap` `Subfield` `Field.toDivisionRing` `SetLike.instMembership` `instSetLike` `SubsemiringClass.toCommSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `SubringClass.toSubsemiringClass` `DivisionRing.toRing` `SubfieldClass.toSubringClass` `instSubfieldClass` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `toAlgebra` `subtype`	—	`SubringClass.toSubsemiringClass` `SubfieldClass.toSubringClass` `instSubfieldClass`
`closure_empty` 📖	mathematical	—	`closure` `Set` `Set.instEmptyCollection` `Bot.bot` `Subfield` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `instCompleteLattice` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder`	—	`GaloisConnection.l_bot` `GaloisInsertion.gc`
`closure_eq` 📖	mathematical	—	`closure` `SetLike.coe` `Subfield` `instSetLike`	—	`GaloisInsertion.l_u_eq`
`closure_eq_of_le` 📖	—	`Set` `Set.instHasSubset` `SetLike.coe` `Subfield` `instSetLike` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `closure`	—	—	`le_antisymm` `closure_le`
`closure_iUnion` 📖	mathematical	—	`closure` `Set.iUnion` `iSup` `Subfield` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `instCompleteLattice`	—	`GaloisConnection.l_iSup` `GaloisInsertion.gc`
`closure_induction` 📖	—	`subset_closure` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `OneMemClass.one_mem` `Subfield` `instSetLike` `AddSubmonoidWithOneClass.toOneMemClass` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `SubsemiringClass.addSubmonoidWithOneClass` `SubringClass.toSubsemiringClass` `SubfieldClass.toSubringClass` `instSubfieldClass` `closure` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `AddMemClass.add_mem` `AddSubmonoidClass.toAddMemClass` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `AddSubgroupClass.toAddSubmonoidClass` `SubringClass.addSubgroupClass` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `NegMemClass.neg_mem` `SubringClass.toNegMemClass` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `GroupWithZero.toDivisionMonoid` `DivisionSemiring.toGroupWithZero` `DivisionRing.toDivisionSemiring` `InvMemClass.inv_mem` `SubfieldClass.toInvMemClass` `Distrib.toMul` `MulMemClass.mul_mem` `SubmonoidClass.toMulMemClass` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `DivisionRing.toDivInvMonoid` `SubgroupClass.toSubmonoidClass` `SubfieldClass.toSubgroupClass` `SetLike.instMembership`	—	—	`subset_closure` `OneMemClass.one_mem` `AddSubmonoidWithOneClass.toOneMemClass` `SubsemiringClass.addSubmonoidWithOneClass` `SubringClass.toSubsemiringClass` `SubfieldClass.toSubringClass` `instSubfieldClass` `AddMemClass.add_mem` `AddSubmonoidClass.toAddMemClass` `AddSubgroupClass.toAddSubmonoidClass` `SubringClass.addSubgroupClass` `NegMemClass.neg_mem` `SubringClass.toNegMemClass` `InvMemClass.inv_mem` `SubfieldClass.toInvMemClass` `MulMemClass.mul_mem` `SubmonoidClass.toMulMemClass` `SubgroupClass.toSubmonoidClass` `SubfieldClass.toSubgroupClass` `ZeroMemClass.zero_mem` `AddSubmonoidClass.toZeroMemClass` `add_neg_cancel` `closure_le`
`closure_le` 📖	mathematical	—	`Subfield` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `closure` `Set` `Set.instHasSubset` `SetLike.coe` `instSetLike`	—	`Set.Subset.trans` `subset_closure` `mem_closure`
`closure_mono` 📖	mathematical	`Set` `Set.instHasSubset`	`Subfield` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `closure`	—	`closure_le` `Set.Subset.trans` `subset_closure`
`closure_preimage_le` 📖	mathematical	—	`Subfield` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `closure` `Set.preimage` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `RingHom.instFunLike` `comap`	—	`closure_le` `SetLike.mem_coe` `mem_comap` `subset_closure`
`closure_sUnion` 📖	mathematical	—	`closure` `Set.sUnion` `iSup` `Subfield` `Set` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `instCompleteLattice` `Set.instMembership`	—	`GaloisConnection.l_sSup` `GaloisInsertion.gc`
`closure_union` 📖	mathematical	—	`closure` `Set` `Set.instUnion` `Subfield` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `instCompleteLattice`	—	`GaloisConnection.l_sup` `GaloisInsertion.gc`
`closure_univ` 📖	mathematical	—	`closure` `Set.univ` `Top.top` `Subfield` `instTop`	—	`closure_eq` `coe_top`
`coe_comap` 📖	mathematical	—	`SetLike.coe` `Subfield` `instSetLike` `comap` `Set.preimage` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `RingHom.instFunLike`	—	—
`coe_iInf` 📖	mathematical	—	`SetLike.coe` `Subfield` `instSetLike` `iInf` `instInfSet` `Set.iInter`	—	`coe_sInf` `Set.biInter_range`
`coe_iSup_of_directed` 📖	mathematical	`Directed` `Subfield` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`SetLike.coe` `instSetLike` `iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `instCompleteLattice` `Set.iUnion`	—	`Set.ext` `mem_iSup_of_directed`
`coe_inf` 📖	mathematical	—	`SetLike.coe` `Subfield` `instSetLike` `instMin` `Set` `Set.instInter` `Subsemigroup.carrier` `MulOne.toMul` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `DivisionRing.toRing` `Submonoid.toSubsemigroup` `Subsemiring.toSubmonoid` `Subring.toSubsemiring` `toSubring`	—	—
`coe_map` 📖	mathematical	—	`SetLike.coe` `Subfield` `instSetLike` `map` `Set.image` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `RingHom.instFunLike`	—	—
`coe_sInf` 📖	mathematical	—	`SetLike.coe` `Subfield` `instSetLike` `InfSet.sInf` `instInfSet` `Set.iInter` `Set` `Set.instMembership`	—	`Set.iInter_congr_Prop` `Set.iInter_exists` `Set.biInter_and'` `Set.iInter_iInter_eq_right`
`coe_sSup_of_directedOn` 📖	mathematical	`Set.Nonempty` `Subfield` `DirectedOn` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`SetLike.coe` `instSetLike` `SupSet.sSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `instCompleteLattice` `Set.iUnion` `Set` `Set.instMembership`	—	`Set.ext` `mem_sSup_of_directedOn`
`coe_top` 📖	mathematical	—	`SetLike.coe` `Subfield` `instSetLike` `Top.top` `instTop` `Set.univ`	—	—
`comap_comap` 📖	mathematical	—	`comap` `RingHom.comp` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring`	—	—
`comap_iInf` 📖	mathematical	—	`comap` `iInf` `Subfield` `instInfSet`	—	`GaloisConnection.u_iInf` `gc_map_comap`
`comap_inf` 📖	mathematical	—	`comap` `Subfield` `instMin`	—	`GaloisConnection.u_inf` `gc_map_comap`
`comap_map` 📖	mathematical	—	`comap` `map`	—	`SetLike.coe_injective` `Set.preimage_image_eq` `RingHom.injective` `DivisionRing.isSimpleRing` `IsSimpleRing.instNontrivial`
`comap_top` 📖	mathematical	—	`comap` `Top.top` `Subfield` `instTop`	—	`GaloisConnection.u_top` `gc_map_comap`
`fieldRange_subtype` 📖	mathematical	—	`RingHom.fieldRange` `Subfield` `SetLike.instMembership` `instSetLike` `toDivisionRing` `subtype`	—	`SetLike.ext'` `RingHom.coe_rangeS` `Subtype.range_coe`
`gc_map_comap` 📖	mathematical	—	`GaloisConnection` `Subfield` `PartialOrder.toPreorder` `instPartialOrder` `map` `comap`	—	`map_le_iff_le_comap`
`instFaithfulSMulSubtypeMem` 📖	mathematical	—	`FaithfulSMul` `Subfield` `SetLike.instMembership` `instSetLike` `instSMulSubtypeMem`	—	`Subsemiring.faithfulSMul`
`instIsScalarTowerSubtypeMem` 📖	mathematical	—	`IsScalarTower` `Subfield` `SetLike.instMembership` `instSetLike` `instSMulSubtypeMem`	—	`Subsemiring.isScalarTower`
`isGLB_sInf` 📖	mathematical	—	`IsGLB` `Subfield` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `InfSet.sInf` `instInfSet`	—	`instIsConcreteLE` `IsGLB.of_image` `coe_sInf` `isGLB_biInf`
`list_prod_mem` 📖	mathematical	`Subfield` `SetLike.instMembership` `instSetLike`	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `DivisionRing.toRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne`	—	`list_prod_mem` `SubgroupClass.toSubmonoidClass` `SubfieldClass.toSubgroupClass` `instSubfieldClass`
`list_sum_mem` 📖	mathematical	`Subfield` `SetLike.instMembership` `instSetLike`	`Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `DivisionRing.toRing` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`list_sum_mem` `AddSubgroupClass.toAddSubmonoidClass` `SubringClass.addSubgroupClass` `SubfieldClass.toSubringClass` `instSubfieldClass`
`map_bot` 📖	mathematical	—	`map` `Bot.bot` `Subfield` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `instCompleteLattice` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder`	—	`GaloisConnection.l_bot` `gc_map_comap`
`map_comap_eq` 📖	mathematical	—	`map` `comap` `Subfield` `instMin` `RingHom.fieldRange`	—	`SetLike.coe_injective` `Set.image_preimage_eq_inter_range`
`map_comap_eq_self` 📖	mathematical	`Subfield` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `RingHom.fieldRange`	`map` `comap`	—	`inf_of_le_left` `map_comap_eq`
`map_comap_eq_self_of_surjective` 📖	mathematical	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `RingHom.instFunLike`	`map` `comap`	—	`SetLike.coe_injective` `Set.image_preimage_eq`
`map_iInf` 📖	mathematical	—	`map` `iInf` `Subfield` `instInfSet`	—	`SetLike.coe_injective` `coe_iInf` `Set.InjOn.image_iInter_eq` `Set.injOn_of_injective` `RingHom.injective` `DivisionRing.isSimpleRing` `IsSimpleRing.instNontrivial`
`map_iSup` 📖	mathematical	—	`map` `iSup` `Subfield` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `instCompleteLattice`	—	`GaloisConnection.l_iSup` `gc_map_comap`
`map_inf` 📖	mathematical	—	`map` `Subfield` `instMin`	—	`SetLike.coe_injective` `Set.image_inter` `RingHom.injective` `DivisionRing.isSimpleRing` `IsSimpleRing.instNontrivial`
`map_le_iff_le_comap` 📖	mathematical	—	`Subfield` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `map` `comap`	—	`Set.image_subset_iff`
`map_map` 📖	mathematical	—	`map` `RingHom.comp` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring`	—	`SetLike.ext'` `Set.image_image`
`map_sup` 📖	mathematical	—	`map` `Subfield` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `instCompleteLattice`	—	`GaloisConnection.l_sup` `gc_map_comap`
`mem_closure` 📖	mathematical	—	`Subfield` `SetLike.instMembership` `instSetLike` `closure`	—	`mem_sInf`
`mem_closure_iff` 📖	mathematical	—	`Subfield` `Field.toDivisionRing` `SetLike.instMembership` `instSetLike` `closure` `Subring` `DivisionRing.toRing` `Subring.instSetLike` `Subring.closure` `DivInvMonoid.toDiv` `DivisionRing.toDivInvMonoid`	—	—
`mem_closure_of_mem` 📖	mathematical	`Set` `Set.instMembership`	`Subfield` `SetLike.instMembership` `instSetLike` `closure`	—	`subset_closure`
`mem_comap` 📖	mathematical	—	`Subfield` `SetLike.instMembership` `instSetLike` `comap` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `RingHom.instFunLike`	—	—
`mem_iInf` 📖	mathematical	—	`Subfield` `SetLike.instMembership` `instSetLike` `iInf` `instInfSet`	—	—
`mem_iSup_of_directed` 📖	mathematical	`Directed` `Subfield` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`SetLike.instMembership` `instSetLike` `iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `instCompleteLattice`	—	`Subring.coe_iSup_of_directed` `Set.mem_iUnion` `inv_mem` `le_antisymm` `iSup_le` `le_iSup` `Set.iUnion_subset`
`mem_inf` 📖	mathematical	—	`Subfield` `SetLike.instMembership` `instSetLike` `instMin`	—	—
`mem_map` 📖	mathematical	—	`Subfield` `SetLike.instMembership` `instSetLike` `map` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `RingHom.instFunLike`	—	—
`mem_sInf` 📖	mathematical	—	`Subfield` `SetLike.instMembership` `instSetLike` `InfSet.sInf` `instInfSet`	—	`Subring.mem_sInf`
`mem_sSup_of_directedOn` 📖	mathematical	`Set.Nonempty` `Subfield` `DirectedOn` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`SetLike.instMembership` `instSetLike` `SupSet.sSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `instCompleteLattice` `Set` `Set.instMembership`	—	`sSup_eq_iSup'` `mem_iSup_of_directed` `Set.Nonempty.to_subtype` `DirectedOn.directed_val`
`mem_top` 📖	mathematical	—	`Subfield` `SetLike.instMembership` `instSetLike` `Top.top` `instTop`	—	`Set.mem_univ`
`multiset_prod_mem` 📖	mathematical	`Subfield` `Field.toDivisionRing` `SetLike.instMembership` `instSetLike`	`Multiset.prod` `CommRing.toCommMonoid` `Field.toCommRing`	—	`multiset_prod_mem` `SubgroupClass.toSubmonoidClass` `SubfieldClass.toSubgroupClass` `instSubfieldClass`
`multiset_sum_mem` 📖	mathematical	`Subfield` `SetLike.instMembership` `instSetLike`	`Multiset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `DivisionRing.toRing`	—	`multiset_sum_mem` `AddSubgroupClass.toAddSubmonoidClass` `SubringClass.addSubgroupClass` `SubfieldClass.toSubringClass` `instSubfieldClass`
`notMem_of_notMem_closure` 📖	mathematical	`Subfield` `SetLike.instMembership` `instSetLike` `closure`	`Set` `Set.instMembership`	—	`subset_closure`
`prod_mem` 📖	mathematical	`Subfield` `Field.toDivisionRing` `SetLike.instMembership` `instSetLike`	`Finset.prod` `CommRing.toCommMonoid` `Field.toCommRing`	—	`prod_mem` `SubgroupClass.toSubmonoidClass` `SubfieldClass.toSubgroupClass` `instSubfieldClass`
`sInf_toSubring` 📖	mathematical	—	`toSubring` `InfSet.sInf` `Subfield` `instInfSet` `iInf` `Subring` `DivisionRing.toRing` `Subring.instInfSet` `Set` `Set.instMembership`	—	`Subring.ext`
`smulCommClass_left` 📖	mathematical	—	`SMulCommClass` `Subfield` `SetLike.instMembership` `instSetLike` `instSMulSubtypeMem`	—	`Subsemiring.smulCommClass_left`
`smulCommClass_right` 📖	mathematical	—	`SMulCommClass` `Subfield` `SetLike.instMembership` `instSetLike` `instSMulSubtypeMem`	—	`Subsemiring.smulCommClass_right`
`smul_def` 📖	mathematical	—	`Subfield` `SetLike.instMembership` `instSetLike` `instSMulSubtypeMem`	—	—
`subring_closure_le` 📖	mathematical	—	`Subring` `DivisionRing.toRing` `Preorder.toLE` `PartialOrder.toPreorder` `Subring.instPartialOrder` `Subring.closure` `toSubring` `closure`	—	`Subring.closure_le` `subset_closure`
`subset_closure` 📖	mathematical	—	`Set` `Set.instHasSubset` `SetLike.coe` `Subfield` `instSetLike` `closure`	—	`mem_closure`
`sum_mem` 📖	mathematical	`Subfield` `SetLike.instMembership` `instSetLike`	`Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `DivisionRing.toRing`	—	`sum_mem` `AddSubgroupClass.toAddSubmonoidClass` `SubringClass.addSubgroupClass` `SubfieldClass.toSubringClass` `instSubfieldClass`

---

← Back to Index