Theorem one_ne_zero

Modification history

2026-09-17 17:14
Mathlib/Algebra/NeZero.lean
feat(Tactic): general tactic to translate `(E)NNReal`, `ENat`, `PNat` goals to `Real` and `Nat` (#43254) …
Modified one_ne_zeroView on Github →
2022-11-17 11:12
Mathlib/Algebra/NeZero.lean
feat: synchronize with mathlib3 #17477 (#577) …
Added one_ne_zeroView on Github →