Irrational

📁 Source: Mathlib/NumberTheory/Real/Irrational.lean

Statistics

Metric	Count
Definitions `instDecidableIrrationalSqrtCastReal`, `instDecidableIrrationalSqrtCastReal_1`, `instDecidableIrrationalSqrtCastReal_2`, `instDecidableIrrationalSqrtOfNatReal`	4
Theorems `not_irrational`, `add_cases`, `add_intCast`, `add_natCast`, `add_ratCast`, `div_cases`, `div_intCast`, `div_natCast`, `div_ratCast`, `intCast_add`, `intCast_div`, `intCast_mul`, `intCast_sub`, `inv`, `mul_cases`, `mul_intCast`, `mul_natCast`, `mul_ratCast`, `natCast_add`, `natCast_div`, `natCast_mul`, `natCast_sub`, `ne_int`, `ne_nat`, `ne_ofNat`, `ne_one`, `ne_rat`, `ne_rational`, `ne_zero`, `neg`, `of_add_intCast`, `of_add_natCast`, `of_add_ratCast`, `of_div_intCast`, `of_div_natCast`, `of_div_ratCast`, `of_intCast_add`, `of_intCast_div`, `of_intCast_mul`, `of_intCast_sub`, `of_inv`, `of_mul_intCast`, `of_mul_natCast`, `of_mul_ratCast`, `of_mul_self`, `of_natCast_add`, `of_natCast_div`, `of_natCast_mul`, `of_natCast_sub`, `of_neg`, `of_one_div`, `of_pow`, `of_ratCast_add`, `of_ratCast_div`, `of_ratCast_mul`, `of_ratCast_sub`, `of_sub_intCast`, `of_sub_natCast`, `of_sub_ratCast`, `of_zpow`, `ratCast_add`, `ratCast_div`, `ratCast_mul`, `ratCast_sub`, `sub_intCast`, `sub_natCast`, `sub_ratCast`, `irrational_sqrt`, `not_irrational`, `not_irrational`, `irrational`, `exists_irrational_btwn`, `exists_rat_of_not_irrational`, `irrational_add_intCast_iff`, `irrational_add_natCast_iff`, `irrational_add_ratCast_iff`, `irrational_div_intCast_iff`, `irrational_div_natCast_iff`, `irrational_div_ratCast_iff`, `irrational_iff_ne_rational`, `irrational_intCast_add_iff`, `irrational_intCast_div_iff`, `irrational_intCast_mul_iff`, `irrational_intCast_sub_iff`, `irrational_inv_iff`, `irrational_mul_intCast_iff`, `irrational_mul_natCast_iff`, `irrational_mul_ratCast_iff`, `irrational_natCast_add_iff`, `irrational_natCast_div_iff`, `irrational_natCast_mul_iff`, `irrational_natCast_sub_iff`, `irrational_neg_iff`, `irrational_nrt_of_n_not_dvd_multiplicity`, `irrational_nrt_of_notint_nrt`, `irrational_ratCast_add_iff`, `irrational_ratCast_div_iff`, `irrational_ratCast_mul_iff`, `irrational_ratCast_sub_iff`, `irrational_sqrt_intCast_iff`, `irrational_sqrt_intCast_iff_of_nonneg`, `irrational_sqrt_natCast_iff`, `irrational_sqrt_ofNat_iff`, `irrational_sqrt_of_multiplicity_odd`, `irrational_sqrt_ratCast_iff`, `irrational_sqrt_ratCast_iff_of_nonneg`, `irrational_sqrt_two`, `irrational_sub_intCast_iff`, `irrational_sub_natCast_iff`, `irrational_sub_ratCast_iff`, `not_irrational_ofNat`, `not_irrational_one`, `not_irrational_zero`, `one_lt_natDegree_of_irrational_root`	114
Total	118

Int

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`not_irrational` 📖	mathematical	—	`Irrational` `Real` `Real.instIntCast`	—	`Irrational.ne_int`

Irrational

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_cases` 📖	—	`Irrational` `Real` `Real.instAdd`	—	—	`Mathlib.Tactic.Contrapose.contrapose₂` `Rat.cast_add` `IsStrictOrderedRing.toCharZero` `Real.instIsStrictOrderedRing`
`add_intCast` 📖	mathematical	`Irrational`	`Real` `Real.instAdd` `Real.instIntCast`	—	`intCast_add` `add_comm`
`add_natCast` 📖	mathematical	`Irrational`	`Real` `Real.instAdd` `Real.instNatCast`	—	`add_intCast`
`add_ratCast` 📖	mathematical	`Irrational`	`Real` `Real.instAdd` `Real.instRatCast`	—	`ratCast_add` `add_comm`
`div_cases` 📖	—	`Irrational` `Real` `DivInvMonoid.toDiv` `Real.instDivInvMonoid`	—	—	`of_inv` `mul_cases`
`div_intCast` 📖	mathematical	`Irrational`	`Real` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instIntCast`	—	`Rat.cast_intCast` `div_ratCast` `Int.cast_ne_zero` `Rat.instCharZero`
`div_natCast` 📖	mathematical	`Irrational`	`Real` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instNatCast`	—	`div_intCast`
`div_ratCast` 📖	mathematical	`Irrational`	`Real` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instRatCast`	—	`div_eq_mul_inv` `Rat.cast_inv` `IsStrictOrderedRing.toCharZero` `Real.instIsStrictOrderedRing` `mul_ratCast` `inv_ne_zero`
`intCast_add` 📖	mathematical	`Irrational`	`Real` `Real.instAdd` `Real.instIntCast`	—	`Rat.cast_intCast` `ratCast_add`
`intCast_div` 📖	mathematical	`Irrational`	`Real` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instIntCast`	—	`intCast_mul` `inv`
`intCast_mul` 📖	mathematical	`Irrational`	`Real` `Real.instMul` `Real.instIntCast`	—	`mul_intCast` `mul_comm`
`intCast_sub` 📖	mathematical	`Irrational`	`Real` `Real.instSub` `Real.instIntCast`	—	`Rat.cast_intCast` `ratCast_sub`
`inv` 📖	mathematical	`Irrational`	`Real` `Real.instInv`	—	`of_inv` `inv_inv`
`mul_cases` 📖	—	`Irrational` `Real` `Real.instMul`	—	—	`Mathlib.Tactic.Contrapose.contrapose₂` `Rat.cast_mul` `IsStrictOrderedRing.toCharZero` `Real.instIsStrictOrderedRing`
`mul_intCast` 📖	mathematical	`Irrational`	`Real` `Real.instMul` `Real.instIntCast`	—	`Rat.cast_intCast` `mul_ratCast` `Int.cast_ne_zero` `Rat.instCharZero`
`mul_natCast` 📖	mathematical	`Irrational`	`Real` `Real.instMul` `Real.instNatCast`	—	`mul_intCast`
`mul_ratCast` 📖	mathematical	`Irrational`	`Real` `Real.instMul` `Real.instRatCast`	—	`of_mul_ratCast` `mul_assoc` `Rat.cast_mul` `IsStrictOrderedRing.toCharZero` `Real.instIsStrictOrderedRing` `mul_inv_cancel₀` `Rat.cast_one` `mul_one`
`natCast_add` 📖	mathematical	`Irrational`	`Real` `Real.instAdd` `Real.instNatCast`	—	`intCast_add`
`natCast_div` 📖	mathematical	`Irrational`	`Real` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instNatCast`	—	`natCast_mul` `inv`
`natCast_mul` 📖	mathematical	`Irrational`	`Real` `Real.instMul` `Real.instNatCast`	—	`intCast_mul`
`natCast_sub` 📖	mathematical	`Irrational`	`Real` `Real.instSub` `Real.instNatCast`	—	`intCast_sub`
`ne_int` 📖	—	`Irrational`	—	—	`Rat.cast_intCast` `ne_rat`
`ne_nat` 📖	—	`Irrational`	—	—	`ne_int`
`ne_ofNat` 📖	—	`Irrational`	—	—	`ne_nat`
`ne_one` 📖	—	`Irrational`	—	—	`Nat.cast_one` `ne_nat`
`ne_rat` 📖	—	`Irrational`	—	—	—
`ne_rational` 📖	—	`Irrational`	—	—	`Rat.cast_div` `IsStrictOrderedRing.toCharZero` `Real.instIsStrictOrderedRing` `Rat.cast_intCast`
`ne_zero` 📖	—	`Irrational`	—	—	`Nat.cast_zero` `ne_nat`
`neg` 📖	mathematical	`Irrational`	`Real` `Real.instNeg`	—	`of_neg` `neg_neg`
`of_add_intCast` 📖	—	`Irrational` `Real` `Real.instAdd` `Real.instIntCast`	—	—	`of_intCast_add` `add_comm`
`of_add_natCast` 📖	—	`Irrational` `Real` `Real.instAdd` `Real.instNatCast`	—	—	`of_add_intCast`
`of_add_ratCast` 📖	—	`Irrational` `Real` `Real.instAdd` `Real.instRatCast`	—	—	`of_ratCast_add` `add_comm`
`of_div_intCast` 📖	—	`Irrational` `Real` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instIntCast`	—	—	`div_cases` `Int.not_irrational`
`of_div_natCast` 📖	—	`Irrational` `Real` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instNatCast`	—	—	`of_div_intCast`
`of_div_ratCast` 📖	—	`Irrational` `Real` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instRatCast`	—	—	`div_cases` `Rat.not_irrational`
`of_intCast_add` 📖	—	`Irrational` `Real` `Real.instAdd` `Real.instIntCast`	—	—	`of_ratCast_add` `Rat.cast_intCast`
`of_intCast_div` 📖	—	`Irrational` `Real` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instIntCast`	—	—	`div_cases` `Int.not_irrational`
`of_intCast_mul` 📖	—	`Irrational` `Real` `Real.instMul` `Real.instIntCast`	—	—	`of_ratCast_mul` `Rat.cast_intCast`
`of_intCast_sub` 📖	—	`Irrational` `Real` `Real.instSub` `Real.instIntCast`	—	—	`of_ratCast_sub` `Rat.cast_intCast`
`of_inv` 📖	—	`Irrational` `Real` `Real.instInv`	—	—	`Rat.cast_inv` `IsStrictOrderedRing.toCharZero` `Real.instIsStrictOrderedRing`
`of_mul_intCast` 📖	—	`Irrational` `Real` `Real.instMul` `Real.instIntCast`	—	—	`of_mul_ratCast` `Rat.cast_intCast`
`of_mul_natCast` 📖	—	`Irrational` `Real` `Real.instMul` `Real.instNatCast`	—	—	`of_mul_intCast`
`of_mul_ratCast` 📖	—	`Irrational` `Real` `Real.instMul` `Real.instRatCast`	—	—	`mul_cases` `Rat.not_irrational`
`of_mul_self` 📖	—	`Irrational` `Real` `Real.instMul`	—	—	`mul_cases`
`of_natCast_add` 📖	—	`Irrational` `Real` `Real.instAdd` `Real.instNatCast`	—	—	`of_intCast_add`
`of_natCast_div` 📖	—	`Irrational` `Real` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instNatCast`	—	—	`of_intCast_div`
`of_natCast_mul` 📖	—	`Irrational` `Real` `Real.instMul` `Real.instNatCast`	—	—	`of_intCast_mul`
`of_natCast_sub` 📖	—	`Irrational` `Real` `Real.instSub` `Real.instNatCast`	—	—	`of_intCast_sub`
`of_neg` 📖	—	`Irrational` `Real` `Real.instNeg`	—	—	`Rat.cast_neg`
`of_one_div` 📖	—	`Irrational` `Real` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instOne`	—	—	`of_ratCast_div` `Rat.cast_one`
`of_pow` 📖	—	`Irrational` `Real` `Monoid.toNatPow` `Real.instMonoid`	—	—	`pow_zero` `Rat.cast_one` `mul_cases` `pow_succ`
`of_ratCast_add` 📖	—	`Irrational` `Real` `Real.instAdd` `Real.instRatCast`	—	—	`add_cases` `Rat.not_irrational`
`of_ratCast_div` 📖	—	`Irrational` `Real` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instRatCast`	—	—	`of_inv` `of_ratCast_mul`
`of_ratCast_mul` 📖	—	`Irrational` `Real` `Real.instMul` `Real.instRatCast`	—	—	`of_mul_ratCast` `mul_comm`
`of_ratCast_sub` 📖	—	`Irrational` `Real` `Real.instSub` `Real.instRatCast`	—	—	`of_neg` `of_ratCast_add` `sub_eq_add_neg`
`of_sub_intCast` 📖	—	`Irrational` `Real` `Real.instSub` `Real.instIntCast`	—	—	`of_sub_ratCast` `Rat.cast_intCast`
`of_sub_natCast` 📖	—	`Irrational` `Real` `Real.instSub` `Real.instNatCast`	—	—	`of_sub_intCast`
`of_sub_ratCast` 📖	—	`Irrational` `Real` `Real.instSub` `Real.instRatCast`	—	—	`of_add_ratCast` `Rat.cast_neg` `sub_eq_add_neg`
`of_zpow` 📖	—	`Irrational` `Real` `DivInvMonoid.toZPow` `Real.instDivInvMonoid`	—	—	`of_pow` `zpow_natCast` `of_inv` `zpow_negSucc`
`ratCast_add` 📖	mathematical	`Irrational`	`Real` `Real.instAdd` `Real.instRatCast`	—	`of_ratCast_add` `Rat.cast_neg` `neg_add_cancel_left`
`ratCast_div` 📖	mathematical	`Irrational`	`Real` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instRatCast`	—	`ratCast_mul` `inv`
`ratCast_mul` 📖	mathematical	`Irrational`	`Real` `Real.instMul` `Real.instRatCast`	—	`mul_ratCast` `mul_comm`
`ratCast_sub` 📖	mathematical	`Irrational`	`Real` `Real.instSub` `Real.instRatCast`	—	`sub_eq_add_neg` `ratCast_add` `neg`
`sub_intCast` 📖	mathematical	`Irrational`	`Real` `Real.instSub` `Real.instIntCast`	—	`Rat.cast_intCast` `sub_ratCast`
`sub_natCast` 📖	mathematical	`Irrational`	`Real` `Real.instSub` `Real.instNatCast`	—	`sub_intCast`
`sub_ratCast` 📖	mathematical	`Irrational`	`Real` `Real.instSub` `Real.instRatCast`	—	`sub_eq_add_neg` `Rat.cast_neg` `add_ratCast`

Nat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`not_irrational` 📖	mathematical	—	`Irrational` `Real` `Real.instNatCast`	—	`Irrational.ne_nat`

Nat.Prime

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`irrational_sqrt` 📖	mathematical	`Nat.Prime`	`Irrational` `Real.sqrt` `Real` `Real.instNatCast`	—	`irrational_sqrt_natCast_iff` `Irreducible.not_isSquare`

Rat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`not_irrational` 📖	mathematical	—	`Irrational` `Real` `Real.instRatCast`	—	—

Transcendental

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`irrational` 📖	mathematical	`Transcendental` `Real` `Rat.commRing` `Real.instRing` `DivisionRing.toRatAlgebra` `Real.instDivisionRing` `IsStrictOrderedRing.toCharZero` `Ring.toSemiring` `DivisionRing.toRing` `Real.partialOrder` `Real.instIsStrictOrderedRing`	`Irrational`	—	`IsStrictOrderedRing.toCharZero` `Real.instIsStrictOrderedRing` `isAlgebraic_algebraMap` `Rat.nontrivial`

(root)

Definitions

Name	Category	Theorems
`instDecidableIrrationalSqrtCastReal` 📖	CompOp	—
`instDecidableIrrationalSqrtCastReal_1` 📖	CompOp	—
`instDecidableIrrationalSqrtCastReal_2` 📖	CompOp	—
`instDecidableIrrationalSqrtOfNatReal` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_irrational_btwn` 📖	mathematical	`Real` `Real.instLT`	`Irrational`	—	`Nat.instAtLeastTwoHAddOfNat` `exists_rat_btwn` `Real.instIsStrictOrderedRing` `Real.instArchimedean` `sub_lt_sub_iff_right` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Irrational.ratCast_add` `irrational_sqrt_two` `sub_lt_iff_lt_add` `lt_sub_iff_add_lt`
`exists_rat_of_not_irrational` 📖	mathematical	`Irrational`	`Real` `Real.instRatCast`	—	—
`irrational_add_intCast_iff` 📖	mathematical	—	`Irrational` `Real` `Real.instAdd` `Real.instIntCast`	—	`Irrational.of_add_intCast` `Irrational.add_intCast`
`irrational_add_natCast_iff` 📖	mathematical	—	`Irrational` `Real` `Real.instAdd` `Real.instNatCast`	—	`Irrational.of_add_natCast` `Irrational.add_natCast`
`irrational_add_ratCast_iff` 📖	mathematical	—	`Irrational` `Real` `Real.instAdd` `Real.instRatCast`	—	`Irrational.of_add_ratCast` `Irrational.add_ratCast`
`irrational_div_intCast_iff` 📖	mathematical	—	`Irrational` `Real` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instIntCast`	—	`Rat.cast_intCast` `irrational_div_ratCast_iff` `Int.cast_ne_zero` `Rat.instCharZero`
`irrational_div_natCast_iff` 📖	mathematical	—	`Irrational` `Real` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instNatCast`	—	`Rat.cast_natCast` `irrational_div_ratCast_iff` `Nat.cast_ne_zero` `Rat.instCharZero`
`irrational_div_ratCast_iff` 📖	mathematical	—	`Irrational` `Real` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instRatCast`	—	`div_eq_mul_inv` `Rat.cast_inv` `IsStrictOrderedRing.toCharZero` `Real.instIsStrictOrderedRing` `irrational_mul_ratCast_iff` `inv_eq_zero`
`irrational_iff_ne_rational` 📖	mathematical	—	`Irrational`	—	`Rat.cast_div` `IsStrictOrderedRing.toCharZero` `Real.instIsStrictOrderedRing` `Rat.cast_intCast`
`irrational_intCast_add_iff` 📖	mathematical	—	`Irrational` `Real` `Real.instAdd` `Real.instIntCast`	—	`Irrational.of_intCast_add` `Irrational.intCast_add`
`irrational_intCast_div_iff` 📖	mathematical	—	`Irrational` `Real` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instIntCast`	—	`div_eq_mul_inv`
`irrational_intCast_mul_iff` 📖	mathematical	—	`Irrational` `Real` `Real.instMul` `Real.instIntCast`	—	`Rat.cast_intCast` `irrational_ratCast_mul_iff` `Int.cast_ne_zero` `Rat.instCharZero`
`irrational_intCast_sub_iff` 📖	mathematical	—	`Irrational` `Real` `Real.instSub` `Real.instIntCast`	—	`Irrational.of_intCast_sub` `Irrational.intCast_sub`
`irrational_inv_iff` 📖	mathematical	—	`Irrational` `Real` `Real.instInv`	—	`Irrational.of_inv` `Irrational.inv`
`irrational_mul_intCast_iff` 📖	mathematical	—	`Irrational` `Real` `Real.instMul` `Real.instIntCast`	—	`Rat.cast_intCast` `irrational_mul_ratCast_iff` `Int.cast_ne_zero` `Rat.instCharZero`
`irrational_mul_natCast_iff` 📖	mathematical	—	`Irrational` `Real` `Real.instMul` `Real.instNatCast`	—	`Rat.cast_natCast` `irrational_mul_ratCast_iff` `Nat.cast_ne_zero` `Rat.instCharZero`
`irrational_mul_ratCast_iff` 📖	mathematical	—	`Irrational` `Real` `Real.instMul` `Real.instRatCast`	—	`mul_comm` `irrational_ratCast_mul_iff`
`irrational_natCast_add_iff` 📖	mathematical	—	`Irrational` `Real` `Real.instAdd` `Real.instNatCast`	—	`Irrational.of_natCast_add` `Irrational.natCast_add`
`irrational_natCast_div_iff` 📖	mathematical	—	`Irrational` `Real` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instNatCast`	—	`div_eq_mul_inv`
`irrational_natCast_mul_iff` 📖	mathematical	—	`Irrational` `Real` `Real.instMul` `Real.instNatCast`	—	`Rat.cast_natCast` `irrational_ratCast_mul_iff` `Nat.cast_ne_zero` `Rat.instCharZero`
`irrational_natCast_sub_iff` 📖	mathematical	—	`Irrational` `Real` `Real.instSub` `Real.instNatCast`	—	`Irrational.of_natCast_sub` `Irrational.natCast_sub`
`irrational_neg_iff` 📖	mathematical	—	`Irrational` `Real` `Real.instNeg`	—	`Irrational.of_neg` `Irrational.neg`
`irrational_nrt_of_n_not_dvd_multiplicity` 📖	mathematical	`Real` `Monoid.toNatPow` `Real.instMonoid` `Real.instIntCast`	`Irrational`	—	`IsStrictOrderedRing.toCharZero` `Real.instIsStrictOrderedRing` `Int.cast_one` `pow_zero` `multiplicity_of_one_right` `isUnit_iff_dvd_one` `Nat.Prime.not_dvd_one` `Fact.out` `irrational_nrt_of_notint_nrt` `zero_pow` `LT.lt.ne'` `FiniteMultiplicity.multiplicity_pow` `Int.instIsCancelMulZero` `Nat.prime_iff_prime_int` `Int.finiteMultiplicity_iff` `Nat.Prime.ne_one` `Int.cast_pow`
`irrational_nrt_of_notint_nrt` 📖	mathematical	`Real` `Monoid.toNatPow` `Real.instMonoid` `Real.instIntCast`	`Irrational`	—	`Int.cast_ne_zero` `IsStrictOrderedRing.toCharZero` `Real.instIsStrictOrderedRing` `pow_ne_zero` `isReduced_of_noZeroDivisors` `IsStrictOrderedRing.noZeroDivisors` `AddGroup.existsAddOfLE` `Dvd.intro_left` `Int.cast_mul` `Int.cast_pow` `div_eq_iff_mul_eq` `div_pow` `Rat.cast_divInt` `Rat.cast_pow` `Rat.divInt_one` `Rat.cast_intCast` `LT.lt.ne'`
`irrational_ratCast_add_iff` 📖	mathematical	—	`Irrational` `Real` `Real.instAdd` `Real.instRatCast`	—	`Irrational.of_ratCast_add` `Irrational.ratCast_add`
`irrational_ratCast_div_iff` 📖	mathematical	—	`Irrational` `Real` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instRatCast`	—	`div_eq_mul_inv`
`irrational_ratCast_mul_iff` 📖	mathematical	—	`Irrational` `Real` `Real.instMul` `Real.instRatCast`	—	`Rat.cast_ne_zero` `IsStrictOrderedRing.toCharZero` `Real.instIsStrictOrderedRing` `left_ne_zero_of_mul` `Irrational.ne_zero` `Irrational.of_ratCast_mul` `Irrational.ratCast_mul`
`irrational_ratCast_sub_iff` 📖	mathematical	—	`Irrational` `Real` `Real.instSub` `Real.instRatCast`	—	`Irrational.of_ratCast_sub` `Irrational.ratCast_sub`
`irrational_sqrt_intCast_iff` 📖	mathematical	—	`Irrational` `Real.sqrt` `Real` `Real.instIntCast` `IsSquare`	—	`Rat.cast_intCast` `irrational_sqrt_ratCast_iff` `Rat.isSquare_intCast_iff` `Int.cast_nonneg_iff` `Rat.instAddLeftMono` `Rat.instZeroLEOneClass` `NeZero.charZero_one` `Rat.instCharZero`
`irrational_sqrt_intCast_iff_of_nonneg` 📖	mathematical	—	`Irrational` `Real.sqrt` `Real` `Real.instIntCast` `IsSquare`	—	`Rat.isSquare_intCast_iff` `irrational_sqrt_ratCast_iff_of_nonneg` `Nat.cast_zero` `Int.cast_zero` `Rat.instAddLeftMono` `Rat.instZeroLEOneClass` `NeZero.charZero_one` `Rat.instCharZero` `Rat.cast_intCast`
`irrational_sqrt_natCast_iff` 📖	mathematical	—	`Irrational` `Real.sqrt` `Real` `Real.instNatCast` `IsSquare`	—	`Rat.isSquare_natCast_iff` `irrational_sqrt_ratCast_iff_of_nonneg` `Nat.cast_nonneg` `IsStrictOrderedRing.toIsOrderedRing` `Rat.instIsStrictOrderedRing` `Rat.cast_natCast`
`irrational_sqrt_ofNat_iff` 📖	mathematical	—	`Irrational` `Real.sqrt` `IsSquare`	—	`irrational_sqrt_natCast_iff`
`irrational_sqrt_of_multiplicity_odd` 📖	mathematical	`multiplicity` `Int.instMonoid`	`Irrational` `Real.sqrt` `Real` `Real.instIntCast`	—	`irrational_nrt_of_n_not_dvd_multiplicity` `ne_of_lt` `Real.sq_sqrt` `Int.cast_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Real.instZeroLEOneClass` `LT.lt.le` `one_ne_zero`
`irrational_sqrt_ratCast_iff` 📖	mathematical	—	`Irrational` `Real.sqrt` `Real` `Real.instRatCast` `IsSquare`	—	`le_or_gt` `irrational_sqrt_ratCast_iff_of_nonneg` `Real.sqrt_eq_zero_of_nonpos` `Rat.cast_nonpos` `Real.instIsStrictOrderedRing` `LT.lt.le`
`irrational_sqrt_ratCast_iff_of_nonneg` 📖	mathematical	—	`Irrational` `Real.sqrt` `Real` `Real.instRatCast` `IsSquare`	—	`Iff.not` `Rat.cast_injective` `IsStrictOrderedRing.toCharZero` `Real.instIsStrictOrderedRing` `Rat.cast_mul` `Real.mul_self_sqrt` `Rat.cast_nonneg` `Real.sqrt_mul_self_eq_abs`
`irrational_sqrt_two` 📖	mathematical	—	`Irrational` `Real.sqrt` `Real` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	—	`Nat.Prime.irrational_sqrt` `Nat.prime_two`
`irrational_sub_intCast_iff` 📖	mathematical	—	`Irrational` `Real` `Real.instSub` `Real.instIntCast`	—	`Irrational.of_sub_intCast` `Irrational.sub_intCast`
`irrational_sub_natCast_iff` 📖	mathematical	—	`Irrational` `Real` `Real.instSub` `Real.instNatCast`	—	`Irrational.of_sub_natCast` `Irrational.sub_natCast`
`irrational_sub_ratCast_iff` 📖	mathematical	—	`Irrational` `Real` `Real.instSub` `Real.instRatCast`	—	`Irrational.of_sub_ratCast` `Irrational.sub_ratCast`
`not_irrational_ofNat` 📖	mathematical	—	`Irrational`	—	`Nat.not_irrational`
`not_irrational_one` 📖	mathematical	—	`Irrational` `Real` `Real.instOne`	—	`Rat.cast_one`
`not_irrational_zero` 📖	mathematical	—	`Irrational` `Real` `Real.instZero`	—	`Rat.cast_zero`
`one_lt_natDegree_of_irrational_root` 📖	mathematical	`Irrational` `DFunLike.coe` `AlgHom` `Polynomial` `CommSemiring.toSemiring` `Int.instCommSemiring` `Real` `Polynomial.semiring` `Real.semiring` `Polynomial.algebraOfAlgebra` `Algebra.id` `Ring.toIntAlgebra` `Real.instRing` `AlgHom.funLike` `Polynomial.aeval` `Real.instZero`	`Polynomial.natDegree` `Int.instSemiring`	—	`Polynomial.exists_eq_X_add_C_of_natDegree_le_one` `not_lt` `eq_intCast` `RingHom.instRingHomClass` `map_add` `SemilinearMapClass.toAddHomClass` `NonUnitalAlgHomClass.instLinearMapClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgHom.algHomClass` `map_mul` `NonUnitalAlgSemiHomClass.toMulHomClass` `map_intCast` `AlgHomClass.toRingHomClass` `Polynomial.aeval_X` `em` `Int.cast_zero` `MulZeroClass.zero_mul` `add_zero` `IsStrictOrderedRing.toCharZero` `Real.instIsStrictOrderedRing` `Rat.instCharZero` `eq_div_iff_mul_eq` `Nat.cast_zero` `mul_comm`

---

← Back to Index