Cardinality

📁 Source: Mathlib/GroupTheory/OreLocalization/Cardinality.lean

Statistics

Metric	Count
Definitions	0
Theorems cardinalMk_le, cardinalMk_le_lift_cardinalMk_of_addCommute, cardinalMk_le_max, numeratorHom_surjective_of_finite, oreSub_zero_surjective_of_finite_left, oreSub_zero_surjective_of_finite_right, cardinalMk_le, cardinalMk_le_lift_cardinalMk_of_commute, cardinalMk_le_max, numeratorHom_surjective_of_finite, oreDiv_one_surjective_of_finite_left, oreDiv_one_surjective_of_finite_right	12
Total	12

AddOreLocalization

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cardinalMk_le 📖	mathematical	—	Cardinal Cardinal.instLE AddOreLocalization AddMonoid.toAddAction	—	Cardinal.lift_id max_eq_right_iff Cardinal.mk_subtype_le cardinalMk_le_max
cardinalMk_le_lift_cardinalMk_of_addCommute 📖	mathematical	AddCommute AddSubmonoid AddMonoid.toAddZeroClass SetLike.instMembership AddSubmonoid.instSetLike AddSubmonoid.add	Cardinal Cardinal.instLE AddOreLocalization Cardinal.lift	—	finite_or_infinite Cardinal.lift_mk_le_lift_mk_of_surjective oreSub_zero_surjective_of_finite_right Cardinal.lift_id' Cardinal.lift_umax oreSub_eq_iff AddSubmonoidClass.toAddMemClass AddSubmonoid.instAddSubmonoidClass SetLike.coe_eq_coe Quotient.mk''_surjective Function.rightInverse_surjInv Cardinal.lift_mk_le_lift_mk_of_injective Cardinal.mul_eq_self Cardinal.aleph0_le_lift Cardinal.lift_mul Cardinal.lift_id Cardinal.mk_prod
cardinalMk_le_max 📖	mathematical	—	Cardinal Cardinal.instLE AddOreLocalization SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder Cardinal.instConditionallyCompleteLinearOrderBot Cardinal.lift AddSubmonoid AddMonoid.toAddZeroClass SetLike.instMembership AddSubmonoid.instSetLike	—	finite_or_infinite Cardinal.lift_mk_le_lift_mk_of_surjective oreSub_zero_surjective_of_finite_right le_max_of_le_right Cardinal.lift_id' Cardinal.lift_umax oreSub_zero_surjective_of_finite_left Cardinal.mk_prod mul_comm Cardinal.mul_eq_max Cardinal.aleph0_le_lift Cardinal.mk_le_of_surjective Quotient.mk''_surjective
numeratorHom_surjective_of_finite 📖	mathematical	—	AddOreLocalization AddMonoid.toAddAction DFunLike.coe AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass instAddMonoid AddMonoidHom.instFunLike numeratorHom	—	oreSub_zero_surjective_of_finite_left
oreSub_zero_surjective_of_finite_left 📖	mathematical	—	AddOreLocalization oreSub AddSubmonoid AddMonoid.toAddZeroClass SetLike.instMembership AddSubmonoid.instSetLike AddSubmonoid.zero	—	ind AddSubmonoid.instAddSubmonoidClass Finite.exists_ne_map_eq_of_infinite instInfiniteNat oreSub_eq_iff AddSemigroupAction.add_vadd add_nsmul add_zero succ_nsmul Ne.lt_of_le not_lt
oreSub_zero_surjective_of_finite_right 📖	mathematical	—	AddOreLocalization oreSub AddSubmonoid AddMonoid.toAddZeroClass SetLike.instMembership AddSubmonoid.instSetLike AddSubmonoid.zero	—	ind AddSubmonoid.instAddSubmonoidClass Finite.exists_ne_map_eq_of_infinite instInfiniteNat oreSub_eq_iff AddSemigroupAction.add_vadd add_nsmul add_zero succ_nsmul Ne.lt_of_le not_lt

OreLocalization

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cardinalMk_le 📖	mathematical	—	Cardinal Cardinal.instLE OreLocalization Monoid.toMulAction	—	Cardinal.lift_id cardinalMk_le_max
cardinalMk_le_lift_cardinalMk_of_commute 📖	mathematical	Commute Submonoid Monoid.toMulOneClass SetLike.instMembership Submonoid.instSetLike Submonoid.mul	Cardinal Cardinal.instLE OreLocalization Cardinal.lift	—	finite_or_infinite Cardinal.lift_mk_le_lift_mk_of_surjective oreDiv_one_surjective_of_finite_right Cardinal.lift_id' Cardinal.lift_umax oreDiv_eq_iff SubmonoidClass.toMulMemClass Submonoid.instSubmonoidClass Quotient.mk''_surjective Function.rightInverse_surjInv Cardinal.lift_mk_le_lift_mk_of_injective Cardinal.mul_eq_self Cardinal.lift_mul Cardinal.lift_id Cardinal.mk_prod
cardinalMk_le_max 📖	mathematical	—	Cardinal Cardinal.instLE OreLocalization SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder Cardinal.instConditionallyCompleteLinearOrderBot Cardinal.lift Submonoid Monoid.toMulOneClass SetLike.instMembership Submonoid.instSetLike	—	finite_or_infinite Cardinal.lift_mk_le_lift_mk_of_surjective oreDiv_one_surjective_of_finite_right le_max_of_le_right Cardinal.lift_id' Cardinal.lift_umax oreDiv_one_surjective_of_finite_left Cardinal.mk_prod mul_comm Cardinal.mul_eq_max Cardinal.mk_le_of_surjective Quotient.mk''_surjective
numeratorHom_surjective_of_finite 📖	mathematical	—	OreLocalization Monoid.toMulAction DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass instMonoid MonoidHom.instFunLike numeratorHom	—	oreDiv_one_surjective_of_finite_left
oreDiv_one_surjective_of_finite_left 📖	mathematical	—	OreLocalization oreDiv Submonoid Monoid.toMulOneClass SetLike.instMembership Submonoid.instSetLike Submonoid.one	—	ind Submonoid.instSubmonoidClass Finite.exists_ne_map_eq_of_infinite instInfiniteNat oreDiv_eq_iff SemigroupAction.mul_smul pow_add mul_one pow_succ Ne.lt_of_le
oreDiv_one_surjective_of_finite_right 📖	mathematical	—	OreLocalization oreDiv Submonoid Monoid.toMulOneClass SetLike.instMembership Submonoid.instSetLike Submonoid.one	—	ind Submonoid.instSubmonoidClass Finite.exists_ne_map_eq_of_infinite instInfiniteNat oreDiv_eq_iff SemigroupAction.mul_smul pow_add mul_one pow_succ Ne.lt_of_le

---

← Back to Index