Niven

📁 Source: Mathlib/NumberTheory/Niven.lean

Statistics

Metric	Count
Definitions	0
Theorems exp_rat_mul_pi_mul_I_pow_two_mul_den, isAlgebraic_cos_rat_mul_pi, isAlgebraic_sin_rat_mul_pi, isAlgebraic_tan_rat_mul_pi, isIntegral_exp_neg_rat_mul_pi_mul_I, isIntegral_exp_rat_mul_pi_mul_I, isIntegral_two_mul_cos_rat_mul_pi, isIntegral_two_mul_sin_rat_mul_pi, exists_int_iff_exists_rat, ratCast_iff, isAlgebraic_cos_rat_mul_pi, isAlgebraic_sin_rat_mul_pi, isAlgebraic_tan_rat_mul_pi, isIntegral_two_mul_cos_rat_mul_pi, isIntegral_two_mul_sin_rat_mul_pi, irrational_cos_rat_mul_pi, isIntegral_two_mul_cos_rat_mul_pi, niven, niven_angle_div_pi_eq, niven_angle_eq, niven_fract_angle_div_pi_eq, niven_sin	22
Total	22

Complex

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exp_rat_mul_pi_mul_I_pow_two_mul_den 📖	mathematical	—	Complex Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero instSemiring exp instMul instRatCast ofReal Real.pi I instOne	—	Rat.num_div_den exp_nat_mul Nat.instAtLeastTwoHAddOfNat Nat.cast_mul Rat.cast_div instCharZero Rat.cast_intCast Rat.cast_natCast Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq IsCancelMulZero.toIsLeftCancelMulZero instIsCancelMulZero Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.NF.mul_eq_eval Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ mul_one Mathlib.Tactic.FieldSimp.NF.div_eq_eval Mathlib.Tactic.FieldSimp.NF.div_eq_eval₁ Mathlib.Tactic.FieldSimp.NF.one_div_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂ Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons_zero one_mul Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div div_one Mathlib.Tactic.FieldSimp.NF.eval_cons Mathlib.Tactic.FieldSimp.zpow'_one Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁ Mathlib.Tactic.FieldSimp.NF.cons_ne_zero Mathlib.Meta.NormNum.isNat_eq_false Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Nat.cast_zero one_ne_zero NeZero.one GroupWithZero.toNontrivial Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.atom_pf exp_int_mul_two_pi_mul_I
isAlgebraic_cos_rat_mul_pi 📖	mathematical	—	IsAlgebraic Complex Int.instCommRing instRing Ring.toIntAlgebra cos instMul instRatCast ofReal Real.pi	—	IsAlgebraic.of_mul NormMulClass.toNoZeroDivisors Int.instNormMulClass Nat.instAtLeastTwoHAddOfNat eq_intCast RingHom.instRingHomClass Int.cast_ofNat NormedDivisionRing.toNormMulClass instNontrivial instCharZero isAlgebraic_algebraMap Int.instNontrivial IsIntegral.isAlgebraic isIntegral_two_mul_cos_rat_mul_pi
isAlgebraic_sin_rat_mul_pi 📖	mathematical	—	IsAlgebraic Complex Int.instCommRing instRing Ring.toIntAlgebra sin instMul instRatCast ofReal Real.pi	—	IsAlgebraic.of_mul NormMulClass.toNoZeroDivisors Int.instNormMulClass Nat.instAtLeastTwoHAddOfNat eq_intCast RingHom.instRingHomClass Int.cast_ofNat NormedDivisionRing.toNormMulClass instNontrivial instCharZero isAlgebraic_algebraMap Int.instNontrivial IsIntegral.isAlgebraic isIntegral_two_mul_sin_rat_mul_pi
isAlgebraic_tan_rat_mul_pi 📖	mathematical	—	IsAlgebraic Complex Int.instCommRing instRing Ring.toIntAlgebra tan instMul instRatCast ofReal Real.pi	—	IsAlgebraic.mul NormMulClass.toNoZeroDivisors Int.instNormMulClass isAlgebraic_sin_rat_mul_pi IsAlgebraic.inv isAlgebraic_cos_rat_mul_pi
isIntegral_exp_neg_rat_mul_pi_mul_I 📖	mathematical	—	IsIntegral Complex Int.instCommRing instRing Ring.toIntAlgebra exp instMul instNeg instRatCast ofReal Real.pi I	—	neg_mul Rat.cast_neg isIntegral_exp_rat_mul_pi_mul_I
isIntegral_exp_rat_mul_pi_mul_I 📖	mathematical	—	IsIntegral Complex Int.instCommRing instRing Ring.toIntAlgebra exp instMul instRatCast ofReal Real.pi I	—	IsIntegral.of_pow Nat.instAtLeastTwoHAddOfNat zero_lt_two Nat.instZeroLEOneClass IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid isIntegral_one exp_rat_mul_pi_mul_I_pow_two_mul_den
isIntegral_two_mul_cos_rat_mul_pi 📖	mathematical	—	IsIntegral Complex Int.instCommRing instRing Ring.toIntAlgebra instMul instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat cos instRatCast ofReal Real.pi	—	Nat.instAtLeastTwoHAddOfNat cos.eq_1 mul_div_cancel₀ two_ne_zero CharZero.NeZero.two instCharZero IsIntegral.add isIntegral_exp_rat_mul_pi_mul_I isIntegral_exp_neg_rat_mul_pi_mul_I
isIntegral_two_mul_sin_rat_mul_pi 📖	mathematical	—	IsIntegral Complex Int.instCommRing instRing Ring.toIntAlgebra instMul instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat sin instRatCast ofReal Real.pi	—	Nat.instAtLeastTwoHAddOfNat sin.eq_1 mul_div_cancel₀ two_ne_zero CharZero.NeZero.two instCharZero IsIntegral.mul IsIntegral.sub isIntegral_exp_neg_rat_mul_pi_mul_I isIntegral_exp_rat_mul_pi_mul_I isIntegral_int_I

IsIntegral

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_int_iff_exists_rat 📖	mathematical	IsIntegral Int.instCommRing DivisionRing.toRing Ring.toIntAlgebra	DivisionRing.toRatCast AddGroupWithOne.toIntCast Ring.toAddGroupWithOne	—	eq_intCast RingHom.instRingHomClass Rat.cast_intCast IsIntegrallyClosed.algebraMap_eq_of_integral Rat.isFractionRing IsIntegralClosure.of_isIntegrallyClosed Localization.isLocalization UniqueFactorizationMonoid.instIsIntegrallyClosed Int.instIsDomain PrincipalIdealRing.to_uniqueFactorizationMonoid EuclideanDomain.to_principal_ideal_domain OreLocalization.instIsScalarTower IsScalarTower.right Algebra.IsIntegral.of_finite AddMonoid.FG.to_moduleFinite_int AddMonoid.fg_of_addGroup_fg AddGroup.instFGInt ratCast_iff
ratCast_iff 📖	mathematical	—	IsIntegral Int.instCommRing DivisionRing.toRing Ring.toIntAlgebra DivisionRing.toRatCast NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing Rat.instNormedField	—	isIntegral_algebraMap_iff AddCommGroup.intIsScalarTower FaithfulSMul.algebraMap_injective instFaithfulSMul_1 DivisionRing.isSimpleRing IsSimpleRing.instNontrivial

Real

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isAlgebraic_cos_rat_mul_pi 📖	mathematical	—	IsAlgebraic Real Int.instCommRing instRing Ring.toIntAlgebra cos instMul instRatCast pi	—	IsAlgebraic.of_mul NormMulClass.toNoZeroDivisors Int.instNormMulClass Nat.instAtLeastTwoHAddOfNat eq_intCast RingHom.instRingHomClass Int.cast_ofNat NormedDivisionRing.toNormMulClass instNontrivial RCLike.charZero_rclike isAlgebraic_algebraMap Int.instNontrivial IsIntegral.isAlgebraic isIntegral_two_mul_cos_rat_mul_pi
isAlgebraic_sin_rat_mul_pi 📖	mathematical	—	IsAlgebraic Real Int.instCommRing instRing Ring.toIntAlgebra sin instMul instRatCast pi	—	IsAlgebraic.of_mul NormMulClass.toNoZeroDivisors Int.instNormMulClass Nat.instAtLeastTwoHAddOfNat eq_intCast RingHom.instRingHomClass Int.cast_ofNat NormedDivisionRing.toNormMulClass instNontrivial RCLike.charZero_rclike isAlgebraic_algebraMap Int.instNontrivial IsIntegral.isAlgebraic isIntegral_two_mul_sin_rat_mul_pi
isAlgebraic_tan_rat_mul_pi 📖	mathematical	—	IsAlgebraic Real Int.instCommRing instRing Ring.toIntAlgebra tan instMul instRatCast pi	—	isAlgebraic_algebraMap_iff AddCommGroup.intIsScalarTower RCLike.ofReal_injective Complex.ofReal_tan Complex.ofReal_mul
isIntegral_two_mul_cos_rat_mul_pi 📖	mathematical	—	IsIntegral Real Int.instCommRing instRing Ring.toIntAlgebra instMul instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat cos instRatCast pi	—	Nat.instAtLeastTwoHAddOfNat isIntegral_algebraMap_iff AddCommGroup.intIsScalarTower RCLike.ofReal_injective Complex.ofReal_mul Complex.ofReal_cos
isIntegral_two_mul_sin_rat_mul_pi 📖	mathematical	—	IsIntegral Real Int.instCommRing instRing Ring.toIntAlgebra instMul instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat sin instRatCast pi	—	Nat.instAtLeastTwoHAddOfNat isIntegral_algebraMap_iff AddCommGroup.intIsScalarTower RCLike.ofReal_injective Complex.ofReal_mul Complex.ofReal_sin

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
irrational_cos_rat_mul_pi 📖	mathematical	—	Irrational Real.cos Real Real.instMul Real.instRatCast Real.pi	—	niven_fract_angle_div_pi_eq exists_rat_of_not_irrational Mathlib.Meta.NormNum.isNat_lt_false IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing Mathlib.Meta.NormNum.isNat_ofNat Tactic.NormNum.isNat_ratDen Mathlib.Meta.NormNum.IsNNRat.to_isRat Mathlib.Meta.NormNum.IsNat.to_isNNRat Rat.den_intFract Mathlib.Meta.NormNum.isNNRat_div Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.isNNRat_inv_pos Rat.instCharZero Tactic.NormNum.nat_gcd_helper_1' Set.mem_singleton_iff
isIntegral_two_mul_cos_rat_mul_pi 📖	mathematical	—	IsIntegral Real Int.instCommRing Real.instRing Ring.toIntAlgebra Real.instMul instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Real.cos Real.instRatCast Real.pi	—	Real.isIntegral_two_mul_cos_rat_mul_pi
niven 📖	mathematical	Real Real.instMul Real.instRatCast Real.pi Real.cos	Set Set.instMembership Set.instInsert Real.instNeg Real.instOne DivInvMonoid.toDiv Real.instDivInvMonoid instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Real.instZero Set.instSingletonSet	—	Nat.instAtLeastTwoHAddOfNat IsIntegral.exists_int_iff_exists_rat RCLike.charZero_rclike Real.isIntegral_two_mul_cos_rat_mul_pi Rat.cast_mul Rat.cast_ofNat Mathlib.Tactic.Linarith.eq_of_not_lt_of_not_gt Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.neg_congr Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Linarith.lt_of_lt_of_eq Mathlib.Tactic.Linarith.sub_neg_of_lt Real.instIsOrderedRing Mathlib.Tactic.Linarith.mul_eq neg_eq_zero sub_eq_zero_of_eq Mathlib.Meta.NormNum.isNat_lt_true Mathlib.Tactic.Ring.add_pf_add_gt Finset.mem_Icc Int.cast_neg Int.cast_ofNat Rat.cast_neg Rat.cast_intCast le_of_not_gt Nat.cast_one Mathlib.Tactic.Linarith.add_lt_of_neg_of_le Real.instIsStrictOrderedRing Mathlib.Tactic.Linarith.lt_of_eq_of_lt Mathlib.Tactic.Linarith.mul_nonpos Mathlib.Tactic.Linarith.sub_nonpos_of_le Real.neg_one_le_cos Real.cos_le_one Int.instCharZero one_div CharP.cast_eq_zero CharP.ofCharZero add_zero neg_div_self NeZero.charZero_one Int.cast_one neg_add_cancel Int.cast_zero zero_div div_self
niven_angle_div_pi_eq 📖	mathematical	Real.cos Real Real.instMul Real.instRatCast Real.pi Set Set.instMembership Set.Icc Rat.instPreorder	Set.instInsert Set.instSingletonSet	—	RCLike.charZero_rclike Function.Injective.mem_set_image smul_left_injective IsDomain.toIsCancelMulZero Rat.isDomain instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors Real.pi_ne_zero mul_le_mul_of_nonneg_right IsOrderedRing.toMulPosMono Real.instIsOrderedRing Nat.cast_zero Real.instIsStrictOrderedRing le_of_lt Real.pi_pos Nat.cast_one Nat.instAtLeastTwoHAddOfNat niven_angle_eq MulZeroClass.zero_mul one_mul Set.image_congr Rat.smul_def one_div Rat.cast_zero Rat.cast_inv Rat.cast_ofNat Rat.cast_div Rat.cast_one
niven_angle_eq 📖	mathematical	Real Real.instMul Real.instRatCast Real.pi Real.cos Set Set.instMembership Set.Icc Real.instPreorder Real.instZero	Set.instInsert DivInvMonoid.toDiv Real.instDivInvMonoid instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Set.instSingletonSet	—	Nat.instAtLeastTwoHAddOfNat niven Real.cos_pi Real.injOn_cos le_of_lt Real.pi_pos le_of_not_gt Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.cast_zero Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero Mathlib.Tactic.Linarith.sub_neg_of_lt Real.instIsOrderedRing IsCancelMulZero.toIsLeftCancelMulZero IsDomain.toIsCancelMulZero Real.instIsDomain Real.cos_pi_sub Real.cos_pi_div_three mul_pos IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing div_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE Mathlib.Meta.Positivity.pos_of_isNat Real.instNontrivial Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Nat.cast_one Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Tactic.Linarith.add_lt_of_neg_of_le CancelDenoms.derive_trans Mathlib.Meta.NormNum.IsNNRat.to_eq Mathlib.Meta.NormNum.isNNRat_div Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.isNNRat_inv_pos RCLike.charZero_rclike CancelDenoms.sub_subst CancelDenoms.mul_subst CancelDenoms.div_subst Mathlib.Meta.NormNum.isNat_eq_true Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNat_mul Mathlib.Tactic.Linarith.mul_neg Mathlib.Meta.NormNum.isNat_lt_true Mathlib.Tactic.Linarith.sub_nonpos_of_le Real.pi_nonneg NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass Real.cos_pi_div_two Mathlib.Tactic.Linarith.mul_nonpos Real.cos_zero Mathlib.Meta.Positivity.nonneg_of_isNat
niven_fract_angle_div_pi_eq 📖	mathematical	Real.cos Real Real.instMul Real.instRatCast Real.pi	Set Set.instMembership Set.instInsert Set.instSingletonSet Int.fract NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing Rat.instNormedField Rat.linearOrder Rat.instFloorRing	—	niven_angle_div_pi_eq Int.fract.eq_1 Rat.cast_sub RCLike.charZero_rclike Rat.cast_intCast Rat.cast_mul Rat.cast_zpow Rat.cast_neg Rat.cast_one sub_mul Real.cos_sub_int_mul_pi Rat.instIsStrictOrderedRing le_of_lt Int.fract_lt_one
niven_sin 📖	mathematical	Real Real.instMul Real.instRatCast Real.pi Real.sin	Set Set.instMembership Set.instInsert Real.instNeg Real.instOne DivInvMonoid.toDiv Real.instDivInvMonoid instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Real.instZero Set.instSingletonSet	—	Nat.instAtLeastTwoHAddOfNat Real.cos_sub_pi_div_two niven Rat.cast_sub RCLike.charZero_rclike Rat.cast_div Rat.cast_one Rat.cast_ofNat Mathlib.Tactic.Linarith.eq_of_not_lt_of_not_gt Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.mul_one Nat.cast_one Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Linarith.lt_of_eq_of_lt Mathlib.Tactic.Linarith.mul_eq Real.instIsOrderedRing neg_eq_zero sub_eq_zero_of_eq Mathlib.Meta.NormNum.isNat_lt_true CancelDenoms.derive_trans Mathlib.Meta.NormNum.IsNNRat.to_eq Mathlib.Meta.NormNum.isNNRat_div Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.isNNRat_inv_pos CancelDenoms.sub_subst CancelDenoms.div_subst Mathlib.Meta.NormNum.isNat_eq_true Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNat_mul CancelDenoms.mul_subst Mathlib.Tactic.Linarith.mul_neg Real.instIsStrictOrderedRing Mathlib.Tactic.Linarith.sub_neg_of_lt

---

← Back to Index