Units

📁 Source: Mathlib/Data/Fintype/Units.lean

Statistics

Metric	Count
Definitions fintype, instFintypeUnitsOfDecidableEq	2
Theorems card_eq_card_units_add_one, card_units, card_units_int, card_eq_card_units_add_one, card_units, univ, instFiniteUnits	7
Total	9

Fintype

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
card_eq_card_units_add_one 📖	mathematical	—	card Units MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero instFintypeUnitsOfDecidableEq	—	card_units tsub_add_cancel_of_le CanonicallyOrderedAdd.toExistsAddOfLE Nat.instCanonicallyOrderedAdd IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid Nat.instOrderedSub card_pos Nontrivial.to_nonempty GroupWithZero.toNontrivial
card_units 📖	mathematical	—	card Units MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero instFintypeUnitsOfDecidableEq	—	Nat.card_eq_fintype_card Nat.card_units
card_units_int 📖	mathematical	—	card Units Int.instMonoid UnitsInt.fintype	—	—

Nat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
card_eq_card_units_add_one 📖	mathematical	—	card Units MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero	—	card_units tsub_add_cancel_of_le CanonicallyOrderedAdd.toExistsAddOfLE instCanonicallyOrderedAdd IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid instOrderedSub card_pos Nontrivial.to_nonempty GroupWithZero.toNontrivial
card_units 📖	mathematical	—	card Units MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero	—	card_congr finite_or_infinite card_sum Finite.of_fintype card_unique Unique.instSubsingleton add_tsub_cancel_left instOrderedSub IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid card_eq_zero_of_infinite Sum.infinite_of_right zero_tsub instCanonicallyOrderedAdd

UnitsInt

Definitions

Name	Category	Theorems
fintype 📖	CompOp	2 math math: univ, Fintype.card_units_int

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
univ 📖	mathematical	—	Finset.univ Units Int.instMonoid fintype Finset Finset.instInsert Units.instDecidableEq Units.instOne Finset.instSingleton Units.instNeg NonUnitalNonAssocRing.toHasDistribNeg NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Int.instCommRing	—	—

(root)

Definitions

Name	Category	Theorems
instFintypeUnitsOfDecidableEq 📖	CompOp	7 math math: Fintype.card_units, card_units_lt, ZMod.card_units, MulChar.sum_one_eq_card_units, LucasLehmer.X.card_units_lt, FiniteField.sum_pow_units, Fintype.card_eq_card_units_add_one

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instFiniteUnits 📖	mathematical	—	Finite Units	—	Finite.of_injective Units.val_injective

---

← Back to Index