Result

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

Statistics

Metric	Count
Definitions rawCast, Result, BoolResult, IsInt, IsNNRat, IsNat, IsRat, Result, Result', eqTrans, isFalse, isInt, isNNRat, isNNRat', isNat, isNegNNRat, isNegNat, isRat, isTrue, ofBoolResult, ofRawInt, ofRawNNRat, ofRawNat, ofRawRat, toInt, toNNRat', toRat, toRat', toRatNZ, toRawEq, toRawIntEq, toSimpResult, inferAddMonoidWithOne, inferRing, inferSemiring, instAddMonoidWithOne, instAddMonoidWithOne', instInhabitedResult, instInhabitedResult', default, instToMessageDataResult, mkOfNat, mkRawIntLit, mkRawRatLit, rawIntLitNatAbs, Result, Result, Result, Result, rawCast, rawCast, rawCast	52
Theorems neg_to_eq, nonneg_to_eq, of_raw, out, to_isNat, to_isRat, to_raw_eq, den_nz, of_raw, to_eq, to_isNat, to_isRat, to_raw_eq, of_raw, out, raw_refl, to_eq, to_isInt, to_isNNRat, to_raw_eq, den_nz, neg_to_eq, of_raw, to_isInt, to_isNNRat, to_raw_eq, instAtLeastTwo, natElim	28
Total	80

Int

Definitions

Name	Category	Theorems
rawCast 📖	CompOp	6 math math: Mathlib.Tactic.Ring.cast_neg, Mathlib.Tactic.RingNF.rat_rawCast_neg, Mathlib.Meta.NormNum.IsInt.to_raw_eq, Mathlib.Meta.NormNum.IsInt.of_raw, Mathlib.Tactic.RingNF.int_rawCast_neg, Mathlib.Tactic.Ring.intCast_negOfNat_Int

Mathlib.Meta.FunProp

Definitions

Name	Category	Theorems
Result 📖	CompData	—

Mathlib.Meta.NormNum

Definitions

Name	Category	Theorems
BoolResult 📖	CompOp	—
IsInt 📖	CompData	31 math math: isInt_pow, Rat.isInt_intFloor, IsRat.to_isInt, IsInt.raw_refl, isintCast, isInt_emod_zero, Rat.isInt_intCeil, isInt_mul, isInt_neg, isInt_inv_neg_one, isInt_sub, isInt_zpow_pos, isInt_ratCast, Rat.IsRat.isInt_round, Rat.isInt_round, isInt_jacobiSymNat, LegendreSym.to_jacobiSym, isInt_negOfNat, isInt_ediv_neg, isInt_rpow_pos, isInt_add, isInt_ediv, IsInt.of_raw, Tactic.ReduceModChar.CharP.isInt_of_mod, isInt_zpow_neg, Tactic.NormNum.isInt_ratNum, isInt_jacobiSym, Rat.isInt_intFloor_ofIsRat_neg, isInt_rpow_neg, IsNat.to_isInt, Rat.isInt_intCeil_ofIsRat_neg
IsNNRat 📖	CompData	21 math math: IsNat.to_isNNRat, isNNRat_ofScientific_of_true, IsNNRat.of_raw, isNNRat_abs_neg, isNNRat_rpow_pos, IsRat.to_isNNRat, Tactic.NormNum.isNNRat_realSqrt_of_isNNRat, isNNRat_zpow_pos, isNNRat_ratCast, IsNNRat.nnreal_rpow_isNNRat, IsNNRat.rpow_isNNRat, isNNRat_inv_pos, Tactic.NormNum.isNNRat_nnrealSqrt_of_isNNRat, isNNRat_abs_nonneg, isNNRat_rpow_neg, isNNRat_zpow_neg, isNNRat_mul, Rat.isNNRat_intFract_of_isNNRat, isNNRat_div, isNNRat_pow, isNNRat_add
IsNat 📖	CompData	79 math math: Tactic.NormNum.isInt_lcm, isNat_ordinalMod, IsNNRat.natFloor, Rat.isNat_intFract_of_isNat, isNat_add, isNat_natAbs_pos, Finset.prod_empty, isNat_inv_zero, Mathlib.Tactic.Ring.add_overlap_pf_zero, isNat_inv_one, isNat_minFac_1, IsNat.nnreal_rpow_isNNRat, isInt_emod_neg, isNat_ordinalNPow, Rat.isNat_intCeil_ofIsNNRat, Tactic.NormNum.isNat_realSqrt, Tactic.NormNum.isNat_sqrt, isNat_descFactorial, IsNat.of_raw, isNat_zpow_pos, IsNNRat.natCeil, Rat.isNat_intCeil, isNat_natSub, IsNat.natCeil, Tactic.ReduceModChar.CharP.isNat_pow, isNat_rpow_neg, IsNat.rpow_isNNRat, isNat_ofNat, Rat.isNat_intFract_of_isInt, IsRat.natFloor, isNat_ordinalMul, isNat_natCast, Rat.isNat_intFloor, isNat_ordinalDiv, isNat_zero, isNat_minFac_3, isNat_descFactorial_zero, Tactic.NormNum.isInt_gcd, IsNat.raw_refl, isNat_fib, isNat_ordinalSub, IsInt.to_isNat, Rat.isNat_intFloor_ofIsNNRat, Finset.sum_empty, IsRat.natCeil, isNat_natDiv, Rat.isNat_round, isNat_ordinalOPow, isNat_ascFactorial, IsNNRat.to_isNat, isNat_natMod, isNat_mul, Tactic.NormNum.isNat_realSqrt_neg, isNat_minFac_4, Tactic.NormNum.isNat_lcm, IsInt.natCeil, IsInt.natFloor, Tactic.NormNum.isNat_ratDen, isNat_neg_of_isNegNat, isNat_one, Tactic.NormNum.isNat_gcd, isNat_minFac_2, isNat_factorial, isNat_natSucc, isNat_natAbs_neg, isInt_ediv_zero, isNat_intOfNat, isNat_ofScientific_of_false, isNat_intCast, isNat_pow, isNat_ratCast, isNat_zpow_neg, IsNat.natFloor, isNat_rpow_pos, isNat_abs_neg, Tactic.NormNum.isNat_realSqrt_of_isRat_negOfNat, Tactic.NormNum.isNat_nnrealSqrt, isInt_emod, isNat_abs_nonneg
IsRat 📖	CompData	18 math math: isRat_inv_pos, isRat_mul, isRat_rpow_pos, IsInt.to_isRat, isRat_rpow_neg, IsNNRat.to_isRat, isRat_ratCast, Rat.isRat_intFract_of_isRat_negOfNat, isRat_mkRat, isRat_zpow_neg, IsRat.of_raw, isRat_zpow_pos, isRat_neg, isRat_div, isRat_inv_neg, isRat_add, isRat_pow, isRat_sub
Result 📖	CompOp	—
Result' 📖	CompData	—
inferAddMonoidWithOne 📖	CompOp	—
inferRing 📖	CompOp	—
inferSemiring 📖	CompOp	—
instAddMonoidWithOne 📖	CompOp	—
instAddMonoidWithOne' 📖	CompOp	—
instInhabitedResult 📖	CompOp	—
instInhabitedResult' 📖	CompOp	—
instToMessageDataResult 📖	CompOp	—
mkOfNat 📖	CompOp	—
mkRawIntLit 📖	CompOp	—
mkRawRatLit 📖	CompOp	—
rawIntLitNatAbs 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instAtLeastTwo 📖	mathematical	—	Nat.AtLeastTwo	—	Nat.instAtLeastTwoHAddOfNat

Mathlib.Meta.NormNum.IsInt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
neg_to_eq 📖	mathematical	Mathlib.Meta.NormNum.IsInt AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup	—	Int.cast_neg Int.cast_natCast
nonneg_to_eq 📖	—	Mathlib.Meta.NormNum.IsInt AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	—	Mathlib.Meta.NormNum.IsNat.to_eq to_isNat
of_raw 📖	mathematical	—	Mathlib.Meta.NormNum.IsInt Int.rawCast	—	—
out 📖	mathematical	Mathlib.Meta.NormNum.IsInt	AddGroupWithOne.toIntCast Ring.toAddGroupWithOne	—	—
to_isNat 📖	mathematical	Mathlib.Meta.NormNum.IsInt	Mathlib.Meta.NormNum.IsNat AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	Int.cast_natCast
to_isRat 📖	mathematical	Mathlib.Meta.NormNum.IsInt	Mathlib.Meta.NormNum.IsRat	—	Nat.cast_one mul_one
to_raw_eq 📖	mathematical	Mathlib.Meta.NormNum.IsInt	Int.rawCast	—	—

Mathlib.Meta.NormNum.IsNNRat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
den_nz 📖	—	Mathlib.Meta.NormNum.IsNNRat DivisionSemiring.toSemiring	—	—	Invertible.ne_zero GroupWithZero.toNontrivial
of_raw 📖	mathematical	—	Mathlib.Meta.NormNum.IsNNRat DivisionSemiring.toSemiring NNRat.rawCast	—	div_eq_mul_inv invOf_eq_inv
to_eq 📖	mathematical	Mathlib.Meta.NormNum.IsNNRat DivisionSemiring.toSemiring AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring	DivInvMonoid.toDiv GroupWithZero.toDivInvMonoid DivisionSemiring.toGroupWithZero	—	invOf_eq_inv div_eq_mul_inv
to_isNat 📖	mathematical	Mathlib.Meta.NormNum.IsNNRat	Mathlib.Meta.NormNum.IsNat AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring	—	Invertible.congr Nat.cast_one invOf_one' mul_one
to_isRat 📖	mathematical	Mathlib.Meta.NormNum.IsNNRat Ring.toSemiring	Mathlib.Meta.NormNum.IsRat	—	Int.cast_natCast
to_raw_eq 📖	mathematical	Mathlib.Meta.NormNum.IsNNRat DivisionSemiring.toSemiring	NNRat.rawCast	—	invOf_eq_inv div_eq_mul_inv

Mathlib.Meta.NormNum.IsNat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_raw 📖	mathematical	—	Mathlib.Meta.NormNum.IsNat Nat.rawCast	—	—
out 📖	mathematical	Mathlib.Meta.NormNum.IsNat	AddMonoidWithOne.toNatCast	—	—
raw_refl 📖	mathematical	—	Mathlib.Meta.NormNum.IsNat Nat.instAddMonoidWithOne	—	—
to_eq 📖	—	Mathlib.Meta.NormNum.IsNat AddMonoidWithOne.toNatCast	—	—	—
to_isInt 📖	mathematical	Mathlib.Meta.NormNum.IsNat AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	Mathlib.Meta.NormNum.IsInt	—	Int.cast_natCast
to_isNNRat 📖	mathematical	Mathlib.Meta.NormNum.IsNat AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring	Mathlib.Meta.NormNum.IsNNRat	—	Nat.cast_one mul_one
to_raw_eq 📖	mathematical	Mathlib.Meta.NormNum.IsNat	Nat.rawCast	—	—

Mathlib.Meta.NormNum.IsRat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
den_nz 📖	—	Mathlib.Meta.NormNum.IsRat DivisionRing.toRing	—	—	Invertible.ne_zero DivisionRing.toNontrivial
neg_to_eq 📖	mathematical	Mathlib.Meta.NormNum.IsRat DivisionRing.toRing AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup DivisionRing.toRing DivInvMonoid.toDiv DivisionRing.toDivInvMonoid	—	Int.cast_negOfNat invOf_eq_inv neg_mul div_eq_mul_inv
of_raw 📖	mathematical	—	Mathlib.Meta.NormNum.IsRat DivisionRing.toRing Rat.rawCast	—	div_eq_mul_inv invOf_eq_inv
to_isInt 📖	mathematical	Mathlib.Meta.NormNum.IsRat	Mathlib.Meta.NormNum.IsInt	—	Invertible.congr Nat.cast_one invOf_one' mul_one
to_isNNRat 📖	mathematical	Mathlib.Meta.NormNum.IsRat	Mathlib.Meta.NormNum.IsNNRat Ring.toSemiring	—	Int.cast_natCast
to_raw_eq 📖	mathematical	Mathlib.Meta.NormNum.IsRat DivisionRing.toRing	Rat.rawCast	—	invOf_eq_inv div_eq_mul_inv

Mathlib.Meta.NormNum.Result

Definitions

Name	Category	Theorems
eqTrans 📖	CompOp	—
isFalse 📖	CompOp	—
isInt 📖	CompOp	—
isNNRat 📖	CompOp	—
isNNRat' 📖	CompOp	—
isNat 📖	CompOp	—
isNegNNRat 📖	CompOp	—
isNegNat 📖	CompOp	—
isRat 📖	CompOp	—
isTrue 📖	CompOp	—
ofBoolResult 📖	CompOp	—
ofRawInt 📖	CompOp	—
ofRawNNRat 📖	CompOp	—
ofRawNat 📖	CompOp	—
ofRawRat 📖	CompOp	—
toInt 📖	CompOp	—
toNNRat' 📖	CompOp	—
toRat 📖	CompOp	—
toRat' 📖	CompOp	—
toRatNZ 📖	CompOp	—
toRawEq 📖	CompOp	—
toRawIntEq 📖	CompOp	—
toSimpResult 📖	CompOp	—

Mathlib.Meta.NormNum.instInhabitedResult'

Definitions

Name	Category	Theorems
default 📖	CompOp	—

Mathlib.Meta.NormNum.isNat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
natElim 📖	—	Mathlib.Meta.NormNum.IsNat Nat.instAddMonoidWithOne	—	—	—

Mathlib.Tactic.BicategoryLike.Eval

Definitions

Name	Category	Theorems
Result 📖	CompData	—

Mathlib.Tactic.BicategoryLike.Normalize

Definitions

Name	Category	Theorems
Result 📖	CompData	—

Mathlib.Tactic.Ring

Definitions

Name	Category	Theorems
Result 📖	CompData	—

Mathlib.Tactic.withResetServerInfo

Definitions

Name	Category	Theorems
Result 📖	CompData	—

NNRat

Definitions

Name	Category	Theorems
rawCast 📖	CompOp	4 math math: Mathlib.Tactic.RingNF.nnrat_rawCast, Mathlib.Meta.NormNum.IsNNRat.of_raw, Mathlib.Tactic.Ring.cast_nnrat, Mathlib.Meta.NormNum.IsNNRat.to_raw_eq

Nat

Definitions

Name	Category	Theorems
rawCast 📖	CompOp	23 math math: Mathlib.Tactic.RingNF.nnrat_rawCast, Mathlib.Tactic.Ring.coeff_one, Mathlib.Tactic.Ring.one_mul, Mathlib.Meta.NormNum.IsNat.of_raw, Mathlib.Tactic.Ring.natCast_int, Mathlib.Tactic.Ring.natCast_nat, Mathlib.Tactic.Ring.atom_pf', Mathlib.Tactic.Ring.one_pow, Mathlib.Tactic.Ring.pow_one_cast, Mathlib.Tactic.RingNF.rat_rawCast_neg, Mathlib.Tactic.Ring.mul_one, Mathlib.Tactic.Ring.const_pos, Mathlib.Tactic.Ring.pow_prod_atom, Mathlib.Tactic.RingNF.nat_rawCast_2, Mathlib.Tactic.Ring.cast_pos, Mathlib.Tactic.RingNF.nat_rawCast_1, Mathlib.Tactic.Ring.atom_pf, Mathlib.Tactic.Ring.toProd_pf, Mathlib.Tactic.RingNF.int_rawCast_neg, Mathlib.Tactic.RingNF.nat_rawCast_0, Mathlib.Meta.NormNum.IsNat.to_raw_eq, Mathlib.Tactic.Ring.pow_zero, Mathlib.Tactic.Ring.pow_atom

Rat

Definitions

Name	Category	Theorems
rawCast 📖	CompOp	4 math math: Mathlib.Tactic.Ring.cast_rat, Mathlib.Meta.NormNum.IsRat.to_raw_eq, Mathlib.Tactic.RingNF.rat_rawCast_neg, Mathlib.Meta.NormNum.IsRat.of_raw

---

← Back to Index