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 sub_eq_add_neg val_add_eq_ite
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 📖	—	—	—	—	Mathlib.Tactic.Contrapose.contrapose₁ LT.lt.le le_trans LE.le.trans_lt' Eq.ge
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