Documentation Verification Report

Fintype

📁 Source: Mathlib/RingTheory/Fintype.lean

Statistics

Metric	Count
Definitions	0
Theorems `univ_of_card_le_three`, `univ_of_card_le_two`, `orderOf_lt`, `card_units_lt`, `natCard_units_lt`, `orderOf_lt_card`	6
Total	6

Finset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`univ_of_card_le_three` 📖	mathematical	`Fintype.card`	`univ` `Finset` `instInsert` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `instSingleton` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup`	—	`eq_of_subset_of_card_le` `subset_univ` `lt_or_eq_of_le` `card_le_card` `univ_of_card_le_two` `Fintype.one_lt_card_iff_nontrivial` `Nat.instAtLeastTwoHAddOfNat` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `Nat.instZeroLEOneClass` `Nat.instCharZero` `card_univ` `card_insert_of_notMem` `zero_ne_one` `NeZero.one` `mem_singleton` `Nat.prime_three` `map_ofNat` `RingEquivClass.toRingHomClass` `RingEquiv.instRingEquivClass` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `one_add_one_eq_two` `add_eq_zero_iff_eq_neg` `Mathlib.Meta.NormNum.isNat_dvd_false` `Mathlib.Meta.NormNum.isNat_ofNat` `ZMod.natCast_eq_zero_iff` `card_singleton` `le_refl`
`univ_of_card_le_two` 📖	mathematical	`Fintype.card`	`univ` `Finset` `instInsert` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `instSingleton` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne`	—	`subsingleton_or_nontrivial` `le_antisymm` `subset_univ` `eq_of_subset_of_card_le` `card_insert_of_notMem` `NeZero.one` `card_singleton`

ZMod

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`orderOf_lt` 📖	mathematical	—	`orderOf` `ZMod` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `commRing`	—	`nontrivial_iff` `LT.lt.ne'` `LT.lt.trans_eq` `orderOf_lt_card` `Finite.of_fintype` `Nat.card_zmod`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`card_units_lt` 📖	mathematical	—	`Fintype.card` `Units` `MonoidWithZero.toMonoid` `instFintypeUnitsOfDecidableEq`	—	`Fintype.card_lt_of_injective_of_notMem` `Units.val_injective` `not_isUnit_zero`
`natCard_units_lt` 📖	mathematical	—	`Nat.card` `Units` `MonoidWithZero.toMonoid`	—	`Fintype.card_eq_nat_card` `card_units_lt`
`orderOf_lt_card` 📖	mathematical	—	`orderOf` `MonoidWithZero.toMonoid` `Nat.card`	—	`IsUnit.unit_spec` `orderOf_units` `LE.le.trans_lt` `orderOf_le_card` `instFiniteUnits` `natCard_units_lt` `orderOf_eq_zero_iff'` `IsUnit.of_pow_eq_one` `LT.lt.ne'` `Nat.card_pos` `Nontrivial.to_nonempty`

---

← Back to Index