Documentation Verification Report

Basic

📁 Source: Mathlib/Algebra/Group/Fin/Basic.lean

Statistics

Metric	Count
Definitions `addCommGroup`, `addCommMonoid`, `addCommSemigroup`, `instAddLeftCancelSemigroup`, `instAddMonoidWithOne`, `instAddRightCancelSemigroup`, `instInvolutiveNeg`	7
Theorems `add_lt_left_iff`, `coe_sub_one`, `instIsCancelAdd`, `intCast_def'`, `le_sub_one_iff`, `lt_add_one_of_succ_lt`, `lt_one_iff`, `lt_sub_iff`, `lt_sub_one_iff`, `neg_last`, `neg_natCast_eq_one`, `rev_add`, `rev_sub`, `sub_le_iff`, `sub_one_lt_iff`	15
Total	22

Fin

Definitions

Name	Category	Theorems
`addCommGroup` 📖	CompOp	1 math math: `BitVec.toFin_zsmul`
`addCommMonoid` 📖	CompOp	2 math math: `isAddFreimanIso_Iio`, `isAddFreimanIso_Iic`
`addCommSemigroup` 📖	CompOp	—
`instAddLeftCancelSemigroup` 📖	CompOp	—
`instAddMonoidWithOne` 📖	CompOp	3 math math: `charP`, `addRothNumber_eq_rothNumberNat`, `BitVec.toFin_nsmul`
`instAddRightCancelSemigroup` 📖	CompOp	—
`instInvolutiveNeg` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_lt_left_iff` 📖	—	—	—	—	`rev_add` `lt_sub_iff`
`coe_sub_one` 📖	—	—	—	—	`sub_zero` `zero_sub` `coe_neg_one` `val_sub_one_of_ne_zero`
`instIsCancelAdd` 📖	mathematical	—	`IsCancelAdd`	—	`add_left_cancel` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `add_right_cancel` `AddRightCancelSemigroup.toIsRightCancelAdd`
`intCast_def'` 📖	—	—	—	—	—
`le_sub_one_iff` 📖	—	—	—	—	`sub_self` `lt_sub_one_iff` `le_iff_lt_or_eq` `val_fin_lt` `sub_eq_iff_eq_add` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `instNeZeroHAddNatOfNat_mathlib` `instIsEmptyFalse`
`lt_add_one_of_succ_lt` 📖	—	—	—	—	`coe_ofNat_eq_mod`
`lt_one_iff` 📖	—	—	—	—	—
`lt_sub_iff` 📖	—	—	—	—	`coe_int_sub_eq_ite`
`lt_sub_one_iff` 📖	—	—	—	—	—
`neg_last` 📖	—	—	—	—	—
`neg_natCast_eq_one` 📖	—	—	—	—	`natCast_eq_last` `neg_last`
`rev_add` 📖	—	—	—	—	`last_sub` `sub_add_eq_sub_sub`
`rev_sub` 📖	—	—	—	—	`rev_eq_iff` `rev_add`
`sub_le_iff` 📖	—	—	—	—	`not_iff_not` `lt_sub_iff`
`sub_one_lt_iff` 📖	—	—	—	—	`not_iff_not`

---

← Back to Index