Basic

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

Statistics

Metric	Count
Definitions `norm_num_lemma_function_equality`, `add`, `mul`, `neg`, `sub`, `evalAdd`, `evalDiv`, `evalFalse`, `evalIntCast`, `evalIntNatAbs`, `evalIntOfNat`, `evalMul`, `evalNatCast`, `evalNatDiv`, `evalNatDvd`, `evalNatMod`, `evalNatSub`, `evalNatSucc`, `evalNeg`, `evalNegOfNat`, `evalNot`, `evalOfNat`, `evalOne`, `evalSub`, `evalTrue`, `evalZero`, `inferDivisionRing`, `inferDivisionSemiring`, `invertibleOfMul`, `invertibleOfMul'`, `monadLiftOptionMetaM`	31
Theorems `raw_refl`, `ble_eq_false`, `eq_of_false`, `eq_of_true`, `isInt_add`, `isInt_eq_true`, `isInt_mul`, `isInt_neg`, `isInt_negOfNat`, `isInt_sub`, `isNNRat_add`, `isNNRat_div`, `isNNRat_eq_true`, `isNNRat_mul`, `isNat_add`, `isNat_dvd_false`, `isNat_dvd_true`, `isNat_eq_true`, `isNat_intCast`, `isNat_intOfNat`, `isNat_mul`, `isNat_natAbs_neg`, `isNat_natAbs_pos`, `isNat_natCast`, `isNat_natDiv`, `isNat_natMod`, `isNat_natSub`, `isNat_natSucc`, `isNat_ofNat`, `isNat_one`, `isNat_zero`, `isRat_add`, `isRat_div`, `isRat_eq_true`, `isRat_mul`, `isRat_neg`, `isRat_sub`, `isintCast`, `ne_of_false_of_true`, `ne_of_true_of_false`	40
Total	71

LibraryNote

Definitions

Name	Category	Theorems
`norm_num_lemma_function_equality` 📖	CompOp	—

Mathlib.Meta

Definitions

Name	Category	Theorems
`monadLiftOptionMetaM` 📖	CompOp	—

Mathlib.Meta.NormNum

Definitions

Name	Category	Theorems
`evalAdd` 📖	CompOp	—
`evalDiv` 📖	CompOp	—
`evalFalse` 📖	CompOp	—
`evalIntCast` 📖	CompOp	—
`evalIntNatAbs` 📖	CompOp	—
`evalIntOfNat` 📖	CompOp	—
`evalMul` 📖	CompOp	—
`evalNatCast` 📖	CompOp	—
`evalNatDiv` 📖	CompOp	—
`evalNatDvd` 📖	CompOp	—
`evalNatMod` 📖	CompOp	—
`evalNatSub` 📖	CompOp	—
`evalNatSucc` 📖	CompOp	—
`evalNeg` 📖	CompOp	—
`evalNegOfNat` 📖	CompOp	—
`evalNot` 📖	CompOp	—
`evalOfNat` 📖	CompOp	—
`evalOne` 📖	CompOp	—
`evalSub` 📖	CompOp	—
`evalTrue` 📖	CompOp	—
`evalZero` 📖	CompOp	—
`inferDivisionRing` 📖	CompOp	—
`inferDivisionSemiring` 📖	CompOp	—
`invertibleOfMul` 📖	CompOp	—
`invertibleOfMul'` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ble_eq_false` 📖	—	—	—	—	—
`eq_of_false` 📖	—	—	—	—	—
`eq_of_true` 📖	—	—	—	—	—
`isInt_add` 📖	—	`Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `IsInt`	—	—	`Int.cast_add`
`isInt_eq_true` 📖	—	`IsInt`	—	—	—
`isInt_mul` 📖	—	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `IsInt`	—	—	`Int.cast_mul`
`isInt_neg` 📖	—	`NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `IsInt`	—	—	`Int.cast_neg`
`isInt_negOfNat` 📖	mathematical	`IsNat` `Nat.instAddMonoidWithOne`	`IsInt` `Int.instRing`	—	`IsNat.out`
`isInt_sub` 📖	—	`SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `IsInt`	—	—	`Int.cast_sub`
`isNNRat_add` 📖	—	`Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `IsNNRat`	—	—	`Nat.cast_mul` `Commute.right_comm` `Commute.invOf_right` `Commute.invOf_left` `Nat.cast_commute` `mul_invOf_cancel_right'` `Nat.cast_add` `add_mul` `Distrib.rightDistribClass` `mul_invOf_cancel_right`
`isNNRat_div` 📖	mathematical	`IsNNRat` `DivisionSemiring.toSemiring` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `GroupWithZero.toDivisionMonoid` `DivisionSemiring.toGroupWithZero`	`DivInvMonoid.toDiv` `GroupWithZero.toDivInvMonoid`	—	`div_eq_mul_inv`
`isNNRat_eq_true` 📖	—	`IsNNRat`	—	—	`Invertible.subsingleton`
`isNNRat_mul` 📖	—	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `IsNNRat`	—	—	`Nat.cast_mul` `Commute.right_comm` `Commute.invOf_right` `Commute.invOf_left` `Nat.cast_commute` `mul_invOf_cancel_right'`
`isNat_add` 📖	—	`AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `AddMonoidWithOne.toAddMonoid` `IsNat`	—	—	`Nat.cast_add`
`isNat_dvd_false` 📖	—	`IsNat` `Nat.instAddMonoidWithOne`	—	—	—
`isNat_dvd_true` 📖	—	`IsNat` `Nat.instAddMonoidWithOne`	—	—	—
`isNat_eq_true` 📖	—	`IsNat`	—	—	—
`isNat_intCast` 📖	mathematical	`IsNat` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Int.instRing`	`AddGroupWithOne.toIntCast`	—	`Int.cast_natCast`
`isNat_intOfNat` 📖	mathematical	`IsNat` `Nat.instAddMonoidWithOne`	`AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Int.instRing`	—	—
`isNat_mul` 📖	—	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `IsNat` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	—	`Nat.cast_mul`
`isNat_natAbs_neg` 📖	mathematical	`IsInt` `Int.instRing`	`IsNat` `Nat.instAddMonoidWithOne`	—	`Int.cast_negOfNat`
`isNat_natAbs_pos` 📖	mathematical	`IsNat` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Int.instRing`	`Nat.instAddMonoidWithOne`	—	—
`isNat_natCast` 📖	mathematical	`IsNat` `Nat.instAddMonoidWithOne`	`AddMonoidWithOne.toNatCast`	—	—
`isNat_natDiv` 📖	—	`IsNat` `Nat.instAddMonoidWithOne`	—	—	—
`isNat_natMod` 📖	—	`IsNat` `Nat.instAddMonoidWithOne`	—	—	—
`isNat_natSub` 📖	—	`IsNat` `Nat.instAddMonoidWithOne`	—	—	—
`isNat_natSucc` 📖	—	`IsNat` `Nat.instAddMonoidWithOne`	—	—	`Nat.cast_add` `Nat.cast_one`
`isNat_ofNat` 📖	mathematical	`AddMonoidWithOne.toNatCast`	`IsNat`	—	—
`isNat_one` 📖	mathematical	—	`IsNat` `AddMonoidWithOne.toOne`	—	`Nat.cast_one`
`isNat_zero` 📖	mathematical	—	`IsNat` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid`	—	`Nat.cast_zero`
`isRat_add` 📖	—	`Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `IsRat`	—	—	`Nat.cast_mul` `Commute.right_comm` `Commute.invOf_right` `Commute.invOf_left` `Nat.cast_commute` `mul_invOf_cancel_right'` `Int.cast_add` `Int.cast_mul` `Int.cast_natCast` `add_mul` `Distrib.rightDistribClass` `mul_invOf_cancel_right`
`isRat_div` 📖	mathematical	`IsRat` `DivisionRing.toRing` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `GroupWithZero.toDivisionMonoid` `DivisionSemiring.toGroupWithZero` `DivisionRing.toDivisionSemiring`	`DivInvMonoid.toDiv` `DivisionRing.toDivInvMonoid`	—	`div_eq_mul_inv`
`isRat_eq_true` 📖	—	`IsRat`	—	—	`Invertible.subsingleton`
`isRat_mul` 📖	—	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `IsRat`	—	—	`Nat.cast_mul` `Commute.right_comm` `Commute.invOf_right` `Commute.invOf_left` `Nat.cast_commute` `Int.cast_mul` `Int.cast_natCast` `mul_invOf_cancel_right'` `mul_invOf_cancel_right`
`isRat_neg` 📖	—	`NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `IsRat`	—	—	`neg_mul` `Int.cast_neg`
`isRat_sub` 📖	—	`SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `IsRat`	—	—	`sub_eq_add_neg` `isRat_add` `isRat_neg` `neg_mul`
`isintCast` 📖	mathematical	`IsInt` `Int.instRing`	`AddGroupWithOne.toIntCast` `Ring.toAddGroupWithOne`	—	—
`ne_of_false_of_true` 📖	—	—	—	—	—
`ne_of_true_of_false` 📖	—	—	—	—	—

Mathlib.Meta.NormNum.IsInt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`raw_refl` 📖	mathematical	—	`Mathlib.Meta.NormNum.IsInt` `Int.instRing`	—	—

Mathlib.Meta.NormNum.Result

Definitions

Name	Category	Theorems
`add` 📖	CompOp	—
`mul` 📖	CompOp	—
`neg` 📖	CompOp	—
`sub` 📖	CompOp	—

---

← Back to Index