Documentation Verification Report

Free

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

Statistics

Metric	Count
Definitions `Free`, `instInfiniteFreeCommRing`, `instInfiniteFreeRing`	3
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`, `instInfiniteFreeGroupOfNonempty`, `instInfiniteFreeMonoidOfNonempty`, `nonempty_commRing`, `nonempty_commRing_iff`, `nonempty_commSemiring_iff`, `nonempty_ring_iff`, `nonempty_semiring_iff`	25
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	21 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`, `Free.congr_left`, `card_edgeFinset_eq_extremalNumber_top_iff_nonempty_iso_turanGraph`, `cliqueFree_iff_top_free`, `Free.congr_right`

(root)

Definitions

Name	Category	Theorems
`instInfiniteFreeCommRing` 📖	CompOp	—
`instInfiniteFreeRing` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instCountableFreeAbelianGroup` 📖	mathematical	—	`Countable` `FreeAbelianGroup`	—	—
`instCountableFreeAddGroup` 📖	mathematical	—	`Countable` `FreeAddGroup`	—	—
`instCountableFreeAddMonoid` 📖	mathematical	—	`Countable` `FreeAddMonoid`	—	—
`instCountableFreeCommRing` 📖	mathematical	—	`Countable` `FreeCommRing`	—	—
`instCountableFreeGroup` 📖	mathematical	—	`Countable` `FreeGroup`	—	—
`instCountableFreeMonoid` 📖	mathematical	—	`Countable` `FreeMonoid`	—	—
`instCountableFreeRing` 📖	mathematical	—	`Countable` `FreeRing`	—	—
`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`	—	—
`instInfiniteFreeGroupOfNonempty` 📖	mathematical	—	`Infinite` `FreeGroup`	—	`Infinite.of_surjective` `instInfiniteNat` `FreeGroup.norm_surjective`
`instInfiniteFreeMonoidOfNonempty` 📖	mathematical	—	`Infinite` `FreeMonoid`	—	—
`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