Inv

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

Statistics

Metric	Count
Definitions Inv, inv, evalInv, evalMkRat, evalRatCast, inferCharZeroOfAddMonoidWithOne, inferCharZeroOfAddMonoidWithOne?, inferCharZeroOfDivisionRing, inferCharZeroOfDivisionRing?, inferCharZeroOfDivisionSemiring?, inferCharZeroOfRing, inferCharZeroOfRing?	12
Theorems isInt_inv_neg_one, isInt_ratCast, isNNRat_inv_pos, isNNRat_ratCast, isNat_inv_one, isNat_inv_zero, isNat_ratCast, isRat_inv_neg, isRat_inv_pos, isRat_mkRat, isRat_ratCast	11
Total	23

Equiv

Definitions

Name	Category	Theorems
Inv 📖	CompOp	1 math math: inv_def

Mathlib.Meta.NormNum

Definitions

Name	Category	Theorems
evalInv 📖	CompOp	—
evalMkRat 📖	CompOp	—
evalRatCast 📖	CompOp	—
inferCharZeroOfAddMonoidWithOne 📖	CompOp	—
inferCharZeroOfAddMonoidWithOne? 📖	CompOp	—
inferCharZeroOfDivisionRing 📖	CompOp	—
inferCharZeroOfDivisionRing? 📖	CompOp	—
inferCharZeroOfDivisionSemiring? 📖	CompOp	—
inferCharZeroOfRing 📖	CompOp	—
inferCharZeroOfRing? 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isInt_inv_neg_one 📖	mathematical	IsInt DivisionRing.toRing	InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid GroupWithZero.toDivisionMonoid DivisionSemiring.toGroupWithZero DivisionRing.toDivisionSemiring	—	Int.cast_negOfNat Nat.cast_one inv_neg inv_one
isInt_ratCast 📖	mathematical	IsInt DivisionRing.toRing Rat.instDivisionRing	DivisionRing.toRatCast	—	Rat.cast_intCast
isNNRat_inv_pos 📖	mathematical	IsNNRat DivisionSemiring.toSemiring	InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid GroupWithZero.toDivisionMonoid DivisionSemiring.toGroupWithZero	—	Nat.cast_ne_zero Nat.cast_add Nat.cast_one invOf_eq_inv mul_inv_rev inv_inv
isNNRat_ratCast 📖	mathematical	IsNNRat Rat.semiring	DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring DivisionRing.toRatCast	—	Nat.cast_one Rat.cast_natCast Rat.cast_one
isNat_inv_one 📖	mathematical	IsNat AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring DivisionSemiring.toSemiring	InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid GroupWithZero.toDivisionMonoid DivisionSemiring.toGroupWithZero	—	Nat.cast_one inv_one
isNat_inv_zero 📖	mathematical	IsNat AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring DivisionSemiring.toSemiring	InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid GroupWithZero.toDivisionMonoid DivisionSemiring.toGroupWithZero	—	Nat.cast_zero inv_zero
isNat_ratCast 📖	mathematical	IsNat AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Rat.instDivisionRing	DivisionRing.toRatCast	—	Rat.cast_natCast
isRat_inv_neg 📖	mathematical	IsRat DivisionRing.toRing	InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid GroupWithZero.toDivisionMonoid DivisionSemiring.toGroupWithZero DivisionRing.toDivisionSemiring	—	Nat.cast_ne_zero Int.cast_neg Int.cast_natCast invOf_eq_inv neg_mul inv_neg mul_inv_rev inv_inv
isRat_inv_pos 📖	mathematical	IsRat DivisionRing.toRing	InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid GroupWithZero.toDivisionMonoid DivisionSemiring.toGroupWithZero DivisionRing.toDivisionSemiring	—	Nat.cast_ne_zero Nat.cast_add Nat.cast_one Int.cast_add Int.cast_natCast Int.cast_one invOf_eq_inv mul_inv_rev inv_inv
isRat_mkRat 📖	—	IsInt Int.instRing IsNat Nat.instAddMonoidWithOne IsRat DivisionRing.toRing Rat.instDivisionRing	—	—	—
isRat_ratCast 📖	mathematical	IsRat DivisionRing.toRing Rat.instDivisionRing	DivisionRing.toRatCast	—	Nat.cast_one Rat.cast_natCast Rat.cast_one Rat.cast_intCast

Mathlib.Meta.NormNum.Result

Definitions

Name	Category	Theorems
inv 📖	CompOp	—

---

← Back to Index