Theorem succ_ne_self

Modification history

2024-03-13 20:53

Mathlib/Algebra/Ring/Basic.lean

chore: remove more autoImplicit (#11336) …

Modified succ_ne_self View on Github →

2022-12-04 13:00

Mathlib/Algebra/Ring/Basic.lean

feat: port algebra.ring.basic (#830) …

Added succ_ne_self View on Github →