Free

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

Statistics

Metric	Count
Definitions Free	1
Theorems mk_abelianization_le, mk_freeAbelianGroup, mk_freeAddGroup, mk_freeAddMonoid, mk_freeCommRing, mk_freeGroup, mk_freeMonoid, mk_freeRing, instCountableFreeAbelianGroup, instCountableFreeAddGroup, instCountableFreeAddMonoid, instCountableFreeCommRing, instCountableFreeGroup, instCountableFreeMonoid, instCountableFreeRing, instInfiniteFreeAbelianGroupOfNonempty, instInfiniteFreeAddGroupOfNonempty, instInfiniteFreeAddMonoidOfNonempty, instInfiniteFreeCommRing, instInfiniteFreeGroupOfNonempty, instInfiniteFreeMonoidOfNonempty, instInfiniteFreeRing, nonempty_commRing, nonempty_commRing_iff, nonempty_commSemiring_iff, nonempty_ring_iff, nonempty_semiring_iff	27
Total	28

Cardinal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mk_abelianization_le 📖	mathematical	—	Cardinal instLE Abelianization	—	mk_le_of_surjective Quotient.mk_surjective
mk_freeAbelianGroup 📖	mathematical	—	FreeAbelianGroup Cardinal SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder instConditionallyCompleteLinearOrderBot aleph0	—	mk_congr mk_finsupp_lift_of_infinite' Int.infinite lift_uzero mk_eq_aleph0 instCountableInt lift_aleph0
mk_freeAddGroup 📖	mathematical	—	FreeAddGroup Cardinal SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder instConditionallyCompleteLinearOrderBot aleph0	—	le_antisymm LE.le.trans_eq mk_le_of_injective FreeAddGroup.toWord_injective Nat.instAtLeastTwoHAddOfNat mk_list_eq_max_mk_aleph0 mk_prod lift_uzero mk_fintype lift_ofNat lt_or_ge max_eq_right LT.lt.le max_eq_right_iff mul_lt_aleph0 natCast_lt_aleph0 max_eq_left LE.le.trans le_mul_right two_ne_zero CharZero.NeZero.two instCharZero mul_eq_left natCast_le_aleph0 OfNat.ofNat_ne_zero max_le FreeAddGroup.of_injective instInfiniteFreeAddGroupOfNonempty
mk_freeAddMonoid 📖	mathematical	—	FreeAddMonoid Cardinal SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder instConditionallyCompleteLinearOrderBot aleph0	—	mk_list_eq_max_mk_aleph0
mk_freeCommRing 📖	mathematical	—	FreeCommRing Cardinal SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder instConditionallyCompleteLinearOrderBot aleph0	—	isEmpty_or_nonempty mk_eq_aleph0 instCountableFreeAbelianGroup Finite.to_countable Finite.of_fintype instInfiniteFreeAbelianGroupOfNonempty mk_eq_zero sup_of_le_right canonicallyOrderedAdd mk_freeAbelianGroup mk_multiset_of_nonempty sup_of_le_left
mk_freeGroup 📖	mathematical	—	FreeGroup Cardinal SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder instConditionallyCompleteLinearOrderBot aleph0	—	le_antisymm LE.le.trans_eq mk_le_of_injective FreeGroup.toWord_injective Nat.instAtLeastTwoHAddOfNat mk_list_eq_max_mk_aleph0 mk_prod lift_uzero mk_fintype lift_ofNat lt_or_ge max_eq_right LT.lt.le mul_lt_aleph0 natCast_lt_aleph0 max_eq_left LE.le.trans le_mul_right two_ne_zero CharZero.NeZero.two instCharZero mul_eq_left natCast_le_aleph0 max_le FreeGroup.of_injective instInfiniteFreeGroupOfNonempty
mk_freeMonoid 📖	mathematical	—	FreeMonoid Cardinal SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder instConditionallyCompleteLinearOrderBot aleph0	—	mk_list_eq_max_mk_aleph0
mk_freeRing 📖	mathematical	—	FreeRing Cardinal SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder instConditionallyCompleteLinearOrderBot aleph0	—	isEmpty_or_nonempty mk_eq_aleph0 instCountableFreeAbelianGroup instCountableFreeMonoid Encodable.countable instInfiniteFreeAbelianGroupOfNonempty mk_eq_zero sup_of_le_right canonicallyOrderedAdd mk_freeAbelianGroup mk_freeMonoid sup_of_le_left

SimpleGraph

Definitions

Name	Category	Theorems
Free 📖	MathDef	19 math math: isExtremal_top_free_iff_isTuranMaximal, free_congr_left, free_of_colorable, free_bot, isExtremal_free_iff, not_free, isExtremal_top_free_turanGraph, extremalNumber_of_fintypeCard_eq, free_congr_right, free_killCopies, free_congr, copyCount_eq_zero, killCopies_eq_left, lt_extremalNumber_iff, labelledCopyCount_eq_zero, lt_extremalNumber_iff_of_nonneg, exists_isExtremal_free, card_edgeFinset_eq_extremalNumber_top_iff_nonempty_iso_turanGraph, cliqueFree_iff_top_free

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instCountableFreeAbelianGroup 📖	mathematical	—	Countable FreeAbelianGroup	—	Quotient.countable instCountableFreeGroup
instCountableFreeAddGroup 📖	mathematical	—	Countable FreeAddGroup	—	Quotient.countable List.countable instCountableProd Bool.countable
instCountableFreeAddMonoid 📖	mathematical	—	Countable FreeAddMonoid	—	List.countable
instCountableFreeCommRing 📖	mathematical	—	Countable FreeCommRing	—	instCountableFreeAbelianGroup Multiset.countable
instCountableFreeGroup 📖	mathematical	—	Countable FreeGroup	—	Quotient.countable List.countable instCountableProd Bool.countable
instCountableFreeMonoid 📖	mathematical	—	Countable FreeMonoid	—	List.countable
instCountableFreeRing 📖	mathematical	—	Countable FreeRing	—	Quotient.countable instCountableFreeGroup instCountableFreeMonoid
instInfiniteFreeAbelianGroupOfNonempty 📖	mathematical	—	Infinite FreeAbelianGroup	—	Equiv.infinite_iff Finsupp.infinite_of_right Int.infinite
instInfiniteFreeAddGroupOfNonempty 📖	mathematical	—	Infinite FreeAddGroup	—	Infinite.of_surjective instInfiniteNat FreeAddGroup.norm_surjective
instInfiniteFreeAddMonoidOfNonempty 📖	mathematical	—	Infinite FreeAddMonoid	—	instInfiniteListOfNonempty
instInfiniteFreeCommRing 📖	mathematical	—	Infinite FreeCommRing	—	instInfiniteFreeAbelianGroupOfNonempty
instInfiniteFreeGroupOfNonempty 📖	mathematical	—	Infinite FreeGroup	—	Infinite.of_surjective instInfiniteNat FreeGroup.norm_surjective
instInfiniteFreeMonoidOfNonempty 📖	mathematical	—	Infinite FreeMonoid	—	instInfiniteListOfNonempty
instInfiniteFreeRing 📖	mathematical	—	Infinite FreeRing	—	instInfiniteFreeAbelianGroupOfNonempty
nonempty_commRing 📖	mathematical	—	CommRing	—	finite_or_infinite nonempty_fintype Cardinal.mk_freeCommRing sup_of_le_left
nonempty_commRing_iff 📖	mathematical	—	CommRing	—	Nonempty.map nonempty_commRing
nonempty_commSemiring_iff 📖	mathematical	—	CommSemiring	—	Nonempty.map nonempty_commRing
nonempty_ring_iff 📖	mathematical	—	Ring	—	Nonempty.map nonempty_commRing
nonempty_semiring_iff 📖	mathematical	—	Semiring	—	Nonempty.map nonempty_commRing

---

← Back to Index