Eq

📁 Source: Mathlib/Tactic/NormNum/Eq.lean

Statistics

Metric	Count
Definitions evalEq	1
Theorems invOf_denom_swap, invOf_denom_swap, isInt_eq_false, isNNRat_eq_false, isNat_eq_false, isRat_eq_false	6
Total	7

Mathlib.Meta.NormNum

Definitions

Name	Category	Theorems
evalEq 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isInt_eq_false 📖	—	IsInt	—	—	—
isNNRat_eq_false 📖	—	IsNNRat	—	—	NNRat.invOf_denom_swap
isNat_eq_false 📖	—	IsNat	—	—	—
isRat_eq_false 📖	—	IsRat	—	—	Rat.invOf_denom_swap Int.cast_natCast

Mathlib.Meta.NormNum.NNRat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
invOf_denom_swap 📖	mathematical	—	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Invertible.invOf AddMonoidWithOne.toOne	—	mul_invOf_eq_iff_eq_mul_right Nat.commute_cast mul_assoc mul_left_eq_iff_eq_invOf_mul

Mathlib.Meta.NormNum.Rat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
invOf_denom_swap 📖	mathematical	—	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing AddGroupWithOne.toIntCast Ring.toAddGroupWithOne Invertible.invOf AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne	—	mul_invOf_eq_iff_eq_mul_right Int.commute_cast mul_assoc mul_left_eq_iff_eq_invOf_mul

---

← Back to Index