IsSquare

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

Statistics

Metric	Count
Definitions IsSquare, evalIsSquareInt, evalIsSquareNat, evalIsSquareRat	4
Theorems iff_isSquare_int_of_isNat, iff_isSquare_of_isInt_int, iff_isSquare_of_isInt_rat, iff_isSquare_of_isNat_rat, isSquare_nat_of_isNat, isSquare_of_isNNRat_rat, not_isSquare_nat_of_isNat, not_isSquare_of_isNNRat_rat_of_den, not_isSquare_of_isNNRat_rat_of_num, not_isSquare_of_isRat_neg	10
Total	14

Mathlib.Meta.NormNum

Definitions

Name	Category	Theorems
evalIsSquareInt 📖	CompOp	—
evalIsSquareNat 📖	CompOp	—
evalIsSquareRat 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
iff_isSquare_int_of_isNat 📖	mathematical	IsNat AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing	IsSquare	—	IsNat.out
iff_isSquare_of_isInt_int 📖	mathematical	IsInt Int.instRing	IsSquare	—	IsInt.out Int.cast_negOfNat Nat.cast_zero neg_zero eq_or_ne MulZeroClass.mul_zero ne_of_lt lt_of_le_of_lt Int.instAddLeftMono IsStrictOrderedRing.toIsOrderedRing Int.instIsStrictOrderedRing mul_self_pos AddGroup.existsAddOfLE IsStrictOrderedRing.toPosMulStrictMono IsStrictOrderedRing.toMulPosStrictMono IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le
iff_isSquare_of_isInt_rat 📖	mathematical	IsInt DivisionRing.toRing Rat.instDivisionRing	IsSquare	—	IsInt.out Int.cast_negOfNat Nat.cast_zero neg_zero eq_or_ne MulZeroClass.mul_zero Rat.instCharZero ne_of_lt lt_of_le_of_lt Rat.instAddLeftMono IsStrictOrderedRing.toIsOrderedRing Rat.instIsStrictOrderedRing mul_self_pos AddGroup.existsAddOfLE IsStrictOrderedRing.toPosMulStrictMono IsStrictOrderedRing.toMulPosStrictMono IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le
iff_isSquare_of_isNat_rat 📖	mathematical	IsNat AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Rat.instDivisionRing	IsSquare	—	IsNat.out
isSquare_nat_of_isNat 📖	mathematical	IsNat Nat.instAddMonoidWithOne	IsSquare	—	IsNat.out
isSquare_of_isNNRat_rat 📖	—	IsSquare IsNNRat Rat.semiring	—	—	IsNNRat.to_eq Nat.cast_mul div_mul_div_comm
not_isSquare_nat_of_isNat 📖	mathematical	IsNat Nat.instAddMonoidWithOne	IsSquare	—	two_ne_zero
not_isSquare_of_isNNRat_rat_of_den 📖	—	IsSquare IsNNRat Rat.semiring	—	—	IsNNRat.to_eq Rat.isSquare_iff Int.cast_natCast Int.isSquare_natCast_iff Rat.den_div_eq_of_coprime Mathlib.Tactic.Contrapose.contrapose₁
not_isSquare_of_isNNRat_rat_of_num 📖	—	IsSquare IsNNRat Rat.semiring	—	—	IsNNRat.to_eq Rat.isSquare_iff Int.cast_natCast Rat.num_div_eq_of_coprime Mathlib.Tactic.Contrapose.contrapose₁
not_isSquare_of_isRat_neg 📖	mathematical	IsRat DivisionRing.toRing Rat.instDivisionRing	IsSquare	—	IsRat.neg_to_eq ne_of_lt Left.neg_neg_iff IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd Rat.instAddLeftMono div_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Rat.instIsStrictOrderedRing IsStrictOrderedRing.toIsOrderedRing Rat.nontrivial mul_self_nonneg AddGroup.existsAddOfLE Rat.instPosMulMono

(root)

Definitions

Name	Category	Theorems
IsSquare 📖	MathDef	89 math math: ZMod.exists_sq_eq_prime_iff_of_mod_four_eq_one, legendreSym.eq_neg_one_iff, Rat.isSquare_intCast_iff, Mathlib.Meta.NormNum.not_isSquare_of_isRat_neg, FiniteField.isSquare_neg_one_iff, FiniteField.isSquare_two_iff, even_ofMul_iff, isSquare_toMul_iff, ZMod.exists_sq_eq_prime_iff_of_mod_four_eq_three, Subgroup.mem_square, ZMod.exists_sq_eq_neg_one_iff, Subsemiring.closure_isSquare, Irreducible.not_isSquare, irrational_sqrt_ratCast_iff, Mathlib.Meta.NormNum.iff_isSquare_of_isInt_int, Rat.isSquare_ofNat_iff, irrational_sqrt_intCast_iff, Nat.eq_sq_add_sq_iff_eq_sq_mul, isSquare_ofAdd_iff, Mathlib.Meta.NormNum.isSquare_nat_of_isNat, ZMod.exists_sq_eq_two_iff, NNReal.isSquare, isSquare_inv, Pell.IsFundamental.d_nonsquare, irrational_sqrt_natCast_iff, ZMod.isSquare_neg_one_iff_forall_mem_primeFactors_mod_four_ne_three, Subgroup.coe_square, irrational_sqrt_ratCast_iff_of_nonneg, AddSubmonoid.closure_isSquare, isSquare_iff_exists_mul_self, Submonoid.mem_square, IsSquare.zero, IsSquare.sq, even_toAdd_iff, Mathlib.Meta.NormNum.iff_isSquare_of_isInt_rat, Prime.not_isSquare, irrational_sqrt_intCast_iff_of_nonneg, FiniteField.isSquare_neg_two_iff, ZMod.nonsquare_of_jacobiSym_eq_neg_one, ZMod.isSquare_neg_one_iff, legendreSym.eq_one_iff, Mathlib.Meta.NormNum.iff_isSquare_of_isNat_rat, isSquare_op_iff, Rat.isSquare_natCast_iff, not_isSquare_of_neg, isSquare_iff_exists_sq, IsSquare.mul_self, FiniteField.exists_nonsquare, FiniteField.unit_isSquare_iff, isSquare_mabs, Even.isSquare_pow, Mathlib.Meta.NormNum.not_isSquare_nat_of_isNat, Rat.isSquare_iff, Subsemigroup.mem_square, isSquare_subset_image_isSquare, isSquare_of_charTwo', IsSquare.one, ZMod.isSquare_neg_one_of_eq_sq_add_sq_of_coprime, Pell.Solution₁.d_nonsquare_of_one_lt_x, Even.isSquare_zpow, legendreSym.eq_one_iff', FiniteField.isSquare_iff, Polynomial.nthRoots_two_eq_zero_iff, FiniteField.isSquare_odd_prime_iff, ZMod.isSquare_neg_one_iff', ZMod.nonsquare_iff_jacobiSym_eq_neg_one, isSquare_unop_iff, Int.isSquare_sign_iff, Pell.exists_iff_not_isSquare, IsRealClosed.nonneg_iff_isSquare, Submonoid.coe_square, legendreSym.eq_neg_one_iff', FiniteField.isSquare_of_char_two, IsRealClosed.isSquare_or_isSquare_neg, Int.isSquare_ofNat_iff, ZMod.isSquare_of_jacobiSym_eq_one, ZMod.isSquare_neg_one_of_eq_sq_add_sq_of_isCoprime, quadraticChar_neg_one_iff_not_isSquare, Mathlib.Meta.NormNum.iff_isSquare_int_of_isNat, Real.isSquare_iff, NonUnitalSubsemiring.closure_isSquare, irrational_sqrt_ofNat_iff, ZMod.euler_criterion, ZMod.exists_sq_eq_neg_two_iff, Int.isSquare_natCast_iff, Complex.isSquare, quadraticChar_one_iff_isSquare, IsSquare.of_nonneg, Subsemigroup.coe_square

---

← Back to Index