Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-04 17:34 858002ba

View on Github →

feat(algebra/char_zero): cast(_pow)_eq_one (#12429)

Estimated changes

added theorem nat.cast_eq_one
added theorem nat.cast_ne_one
added theorem nat.cast_pow_eq_one