Sqrt

📁 Source: Mathlib/Data/Rat/Sqrt.lean

Statistics

Metric	Count
Definitions instDecidablePredIsSquare	1
Theorems exists_mul_self, sqrt_eq, sqrt_intCast, sqrt_natCast, sqrt_nonneg, sqrt_ofNat	6
Total	7

Rat

Definitions

Name	Category	Theorems
instDecidablePredIsSquare 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_mul_self 📖	mathematical	—	sqrt	—	sqrt_eq abs_mul_abs_self
sqrt_eq 📖	mathematical	—	sqrt abs instLattice addGroup	—	sqrt.eq_1 mul_self_num mul_self_den Int.sqrt_eq Nat.sqrt_eq abs_def
sqrt_intCast 📖	mathematical	—	sqrt Int.sqrt	—	—
sqrt_natCast 📖	mathematical	—	sqrt	—	Int.cast_natCast sqrt_intCast Int.sqrt_natCast
sqrt_nonneg 📖	mathematical	—	sqrt	—	mkRat_nonneg Int.sqrt_nonneg
sqrt_ofNat 📖	mathematical	—	sqrt	—	sqrt_natCast

---

← Back to Index