Theorem Irrational.ne_ofNat

Modification history

2025-01-02 08:45

Mathlib/Data/Real/Irrational.lean

chore: use `ofNat()` around `Real` and `Complex` (#20388) …

Modified Irrational.ne_ofNat View on Github →

2024-06-18 08:57

Mathlib/Data/Real/Irrational.lean

feat: `Irrational √q` iff `¬IsSquare q` for `Nat`/`Int`/`Rat` (#13867) …

Added Irrational.ne_ofNat View on Github →