Cardinal

📁 Source: Mathlib/RingTheory/HahnSeries/Cardinal.lean

Statistics

Metric	Count
Definitions `cardSupp`, `cardSuppLTAddSubgroup`, `cardSuppLTAddSubmonoid`, `cardSuppLTSubfield`, `cardSuppLTSubring`	5
Theorems `cardSuppLTSubfield_carrier`, `cardSupp_add_le`, `cardSupp_congr`, `cardSupp_div_le`, `cardSupp_hsum_le`, `cardSupp_hsum_powers_le`, `cardSupp_inv_le`, `cardSupp_map_le`, `cardSupp_mono`, `cardSupp_mul_le`, `cardSupp_mul_single_le`, `cardSupp_neg`, `cardSupp_neg_le`, `cardSupp_one`, `cardSupp_one_le`, `cardSupp_pow_le`, `cardSupp_single_le`, `cardSupp_single_mul_le`, `cardSupp_single_of_ne`, `cardSupp_smul_le`, `cardSupp_sub_le`, `cardSupp_truncLT_le`, `cardSupp_zero`, `coe_cardSuppLTAddSubgroup`, `coe_cardSuppLTAddSubmonoid`, `mem_cardSuppLTAddSubgroup`, `mem_cardSuppLTAddSubmonoid`, `mem_cardSuppLTSubfield`, `mem_cardSuppLTSubring`	29
Total	34

HahnSeries

Definitions

Name	Category	Theorems
`cardSupp` 📖	CompOp	28 math math: `mem_cardSuppLTSubfield`, `cardSupp_single_of_ne`, `coe_cardSuppLTAddSubmonoid`, `cardSupp_smul_le`, `cardSupp_single_le`, `cardSupp_congr`, `cardSupp_truncLT_le`, `cardSupp_one_le`, `cardSupp_map_le`, `mem_cardSuppLTSubring`, `cardSupp_neg_le`, `mem_cardSuppLTAddSubgroup`, `cardSupp_neg`, `coe_cardSuppLTAddSubgroup`, `cardSupp_div_le`, `cardSupp_mul_single_le`, `cardSupp_single_mul_le`, `cardSupp_zero`, `mem_cardSuppLTAddSubmonoid`, `cardSupp_mono`, `cardSupp_add_le`, `cardSupp_sub_le`, `cardSupp_hsum_powers_le`, `cardSupp_inv_le`, `cardSupp_hsum_le`, `cardSupp_one`, `cardSupp_pow_le`, `cardSupp_mul_le`
`cardSuppLTAddSubgroup` 📖	CompOp	3 math math: `cardSuppLTSubfield_carrier`, `mem_cardSuppLTAddSubgroup`, `coe_cardSuppLTAddSubgroup`
`cardSuppLTAddSubmonoid` 📖	CompOp	2 math math: `coe_cardSuppLTAddSubmonoid`, `mem_cardSuppLTAddSubmonoid`
`cardSuppLTSubfield` 📖	CompOp	2 math math: `mem_cardSuppLTSubfield`, `cardSuppLTSubfield_carrier`
`cardSuppLTSubring` 📖	CompOp	1 math math: `mem_cardSuppLTSubring`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cardSuppLTSubfield_carrier` 📖	mathematical	—	`SetLike.coe` `Subfield` `HahnSeries` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `Field.toDivisionRing` `instField` `Subfield.instSetLike` `cardSuppLTSubfield` `AddSubsemigroup.carrier` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `instAddGroup` `AddSubmonoid.toAddSubsemigroup` `AddSubgroup.toAddSubmonoid` `cardSuppLTAddSubgroup`	—	—
`cardSupp_add_le` 📖	mathematical	—	`Cardinal` `Cardinal.instLE` `cardSupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `HahnSeries` `instAdd` `Cardinal.instAdd`	—	`LE.le.trans` `Cardinal.mk_le_mk_of_subset` `support_add_subset` `Cardinal.mk_union_le`
`cardSupp_congr` 📖	mathematical	`support`	`cardSupp`	—	—
`cardSupp_div_le` 📖	mathematical	—	`Cardinal` `Cardinal.instLE` `cardSupp` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `HahnSeries` `DivInvMonoid.toDiv` `instDivInvMonoid` `Cardinal.instMul` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `Cardinal.instConditionallyCompleteLinearOrderBot` `Cardinal.aleph0`	—	`LE.le.trans` `IsOrderedAddMonoid.toIsOrderedCancelAddMonoid` `cardSupp_mul_le` `mul_le_mul_right` `CanonicallyOrderedAdd.toMulLeftMono` `Cardinal.canonicallyOrderedAdd` `cardSupp_inv_le`
`cardSupp_hsum_le` 📖	mathematical	—	`Cardinal` `Cardinal.instLE` `Cardinal.lift` `cardSupp` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `SummableFamily.hsum` `Cardinal.sum` `DFunLike.coe` `SummableFamily` `HahnSeries` `SummableFamily.instFunLike`	—	`LE.le.trans` `Cardinal.lift_le` `Cardinal.mk_le_mk_of_subset` `SummableFamily.support_hsum_subset` `Cardinal.mk_iUnion_le_sum_mk_lift`
`cardSupp_hsum_powers_le` 📖	mathematical	—	`Cardinal` `Cardinal.instLE` `cardSupp` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `SummableFamily.hsum` `SummableFamily.powers` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `Cardinal.instConditionallyCompleteLinearOrderBot` `Cardinal.aleph0` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`Cardinal.lift_uzero` `le_imp_le_of_le_of_le` `le_refl` `Cardinal.sum_pow_le_max_aleph0` `cardSupp_hsum_le` `Cardinal.sum_le_sum` `SummableFamily.powers_toFun` `cardSupp_pow_le` `pow_zero` `zero_pow` `cardSupp_zero` `Cardinal.canonicallyOrderedAdd`
`cardSupp_inv_le` 📖	mathematical	—	`Cardinal` `Cardinal.instLE` `cardSupp` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `HahnSeries` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroupWithZero.toDivisionCommMonoid` `Semifield.toCommGroupWithZero` `Field.toSemifield` `instField` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `Cardinal.instConditionallyCompleteLinearOrderBot` `Cardinal.aleph0`	—	`eq_or_ne` `inv_zero` `cardSupp_zero` `sup_of_le_left` `Cardinal.canonicallyOrderedAdd` `LE.le.trans` `cardSupp_single_mul_le` `cardSupp_hsum_powers_le` `sup_le_sup` `le_refl` `LE.le.trans'` `IsOrderedAddMonoid.toIsOrderedCancelAddMonoid` `cardSupp_mono` `coeff_single_mul` `sub_neg_eq_add` `IsDomain.to_noZeroDivisors` `Field.isDomain` `MulZeroClass.mul_zero` `sub_zero` `NeZero.one` `IsSimpleRing.instNontrivial` `DivisionRing.isSimpleRing` `coeff_one` `zero_add`
`cardSupp_map_le` 📖	mathematical	—	`Cardinal` `Cardinal.instLE` `cardSupp` `map` `ZeroHom` `ZeroHom.funLike` `ZeroHom.zeroHomClass`	—	`cardSupp_mono` `ZeroHom.zeroHomClass` `support_map_subset`
`cardSupp_mono` 📖	mathematical	`Set` `Set.instHasSubset` `support`	`Cardinal` `Cardinal.instLE` `cardSupp`	—	`Cardinal.mk_le_mk_of_subset`
`cardSupp_mul_le` 📖	mathematical	—	`Cardinal` `Cardinal.instLE` `cardSupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `HahnSeries` `instMul` `Cardinal.instMul`	—	`LE.le.trans` `Cardinal.mk_le_mk_of_subset` `support_mul_subset` `Cardinal.mk_add_le`
`cardSupp_mul_single_le` 📖	mathematical	—	`Cardinal` `Cardinal.instLE` `cardSupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `HahnSeries` `instMul` `DFunLike.coe` `ZeroHom` `instZero` `ZeroHom.funLike` `single`	—	`mul_one` `LE.le.trans` `cardSupp_mul_le` `mul_le_mul_right` `CanonicallyOrderedAdd.toMulLeftMono` `Cardinal.canonicallyOrderedAdd` `cardSupp_single_le`
`cardSupp_neg` 📖	mathematical	—	`cardSupp` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `HahnSeries` `instNeg`	—	`cardSupp_congr` `support_neg`
`cardSupp_neg_le` 📖	mathematical	—	`Cardinal` `Cardinal.instLE` `cardSupp` `NegZeroClass.toZero` `HahnSeries` `instNeg`	—	`cardSupp_mono` `support_neg_subset`
`cardSupp_one` 📖	mathematical	—	`cardSupp` `HahnSeries` `instOne` `Cardinal` `Cardinal.instOne`	—	`cardSupp_single_of_ne` `one_ne_zero`
`cardSupp_one_le` 📖	mathematical	—	`Cardinal` `Cardinal.instLE` `cardSupp` `HahnSeries` `instOne` `Cardinal.instOne`	—	`cardSupp_single_le`
`cardSupp_pow_le` 📖	mathematical	—	`Cardinal` `Cardinal.instLE` `cardSupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `HahnSeries` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instSemiring` `CommSemiring.toSemiring` `Cardinal.commSemiring`	—	`pow_zero` `pow_succ` `LE.le.trans` `cardSupp_mul_le` `mul_le_mul_left` `covariant_swap_mul_of_covariant_mul` `CanonicallyOrderedAdd.toMulLeftMono` `Cardinal.canonicallyOrderedAdd`
`cardSupp_single_le` 📖	mathematical	—	`Cardinal` `Cardinal.instLE` `cardSupp` `DFunLike.coe` `ZeroHom` `HahnSeries` `instZero` `ZeroHom.funLike` `single` `Cardinal.instOne`	—	`LE.le.trans_eq` `Cardinal.mk_le_mk_of_subset` `support_single_subset` `Cardinal.mk_singleton`
`cardSupp_single_mul_le` 📖	mathematical	—	`Cardinal` `Cardinal.instLE` `cardSupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `HahnSeries` `instMul` `DFunLike.coe` `ZeroHom` `instZero` `ZeroHom.funLike` `single`	—	`one_mul` `LE.le.trans` `cardSupp_mul_le` `mul_le_mul_left` `covariant_swap_mul_of_covariant_mul` `CanonicallyOrderedAdd.toMulLeftMono` `Cardinal.canonicallyOrderedAdd` `cardSupp_single_le`
`cardSupp_single_of_ne` 📖	mathematical	—	`cardSupp` `DFunLike.coe` `ZeroHom` `HahnSeries` `instZero` `ZeroHom.funLike` `single` `Cardinal` `Cardinal.instOne`	—	`cardSupp.eq_1` `support_single_of_ne` `Cardinal.mk_singleton`
`cardSupp_smul_le` 📖	mathematical	—	`Cardinal` `Cardinal.instLE` `cardSupp` `HahnSeries` `instSMul`	—	`cardSupp_mono` `support_smul_subset`
`cardSupp_sub_le` 📖	mathematical	—	`Cardinal` `Cardinal.instLE` `cardSupp` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `HahnSeries` `instSub` `Cardinal.instAdd`	—	`LE.le.trans` `Cardinal.mk_le_mk_of_subset` `support_sub_subset` `Cardinal.mk_union_le`
`cardSupp_truncLT_le` 📖	mathematical	—	`Cardinal` `Cardinal.instLE` `cardSupp` `DFunLike.coe` `ZeroHom` `HahnSeries` `instZero` `ZeroHom.funLike` `truncLT`	—	`cardSupp_mono` `support_truncLT_subset`
`cardSupp_zero` 📖	mathematical	—	`cardSupp` `HahnSeries` `instZero` `Cardinal` `Cardinal.instZero`	—	`support_zero` `Cardinal.mk_eq_zero` `Set.instIsEmptyElemEmptyCollection`
`coe_cardSuppLTAddSubgroup` 📖	mathematical	—	`SetLike.coe` `AddSubgroup` `HahnSeries` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `instAddGroup` `AddSubgroup.instSetLike` `cardSuppLTAddSubgroup` `setOf` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `Cardinal` `Preorder.toLT` `PartialOrder.toPreorder` `Cardinal.partialOrder` `cardSupp`	—	—
`coe_cardSuppLTAddSubmonoid` 📖	mathematical	—	`SetLike.coe` `AddSubmonoid` `HahnSeries` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `instAddMonoid` `AddSubmonoid.instSetLike` `cardSuppLTAddSubmonoid` `setOf` `Cardinal` `Preorder.toLT` `PartialOrder.toPreorder` `Cardinal.partialOrder` `cardSupp`	—	—
`mem_cardSuppLTAddSubgroup` 📖	mathematical	—	`HahnSeries` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `AddSubgroup` `instAddGroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `cardSuppLTAddSubgroup` `Cardinal` `Preorder.toLT` `PartialOrder.toPreorder` `Cardinal.partialOrder` `cardSupp`	—	—
`mem_cardSuppLTAddSubmonoid` 📖	mathematical	—	`HahnSeries` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddSubmonoid` `instAddMonoid` `SetLike.instMembership` `AddSubmonoid.instSetLike` `cardSuppLTAddSubmonoid` `Cardinal` `Preorder.toLT` `PartialOrder.toPreorder` `Cardinal.partialOrder` `cardSupp`	—	—
`mem_cardSuppLTSubfield` 📖	mathematical	—	`HahnSeries` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `Subfield` `Field.toDivisionRing` `instField` `SetLike.instMembership` `Subfield.instSetLike` `cardSuppLTSubfield` `Cardinal` `Preorder.toLT` `PartialOrder.toPreorder` `Cardinal.partialOrder` `cardSupp`	—	—
`mem_cardSuppLTSubring` 📖	mathematical	—	`HahnSeries` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Subring` `instRing` `SetLike.instMembership` `Subring.instSetLike` `cardSuppLTSubring` `Cardinal` `Preorder.toLT` `PartialOrder.toPreorder` `Cardinal.partialOrder` `cardSupp`	—	—

---

← Back to Index