Mathlib v3 is deprecated. Go to Mathlib v4

Theorem add_self_eq_zero

Modification history

2020-10-08 10:23

src/algebra/char_zero.lean

chore(algebra/char_zero): rename vars, add `with_top` instance (#4523) …

Modified add_self_eq_zero View on Github →

2018-01-21 23:57

algebra/char_zero.lean

feat(data/real): real square root function, sqrt 2 is irrational

Added add_self_eq_zero View on Github →