Commit 2023-01-09 16:42 e1bccd6e

View on Github →

chore(data/int/order/basic): Fix lemma name (#17967) int.coe_nat_abs wasn't referring to the correct lemma. Change the name, add the lemma it should correspond to and tag both with simp and norm_cast.

Estimated changes

Modified archive/imo/imo2013_q5.lean

Modified src/algebra/euclidean_domain/instances.lean

Modified src/algebra/group_power/lemmas.lean

modified theorem int.nat_abs_sq

Modified src/analysis/normed/field/basic.lean

Modified src/data/int/basic.lean

modified theorem int.nat_abs_mul_self'

Modified src/data/int/dvd/basic.lean

Modified src/data/int/order/basic.lean

added theorem int.abs_coe_nat

modified theorem int.coe_nat_abs

added theorem nat.cast_nat_abs

Modified src/data/rat/floor.lean

Modified src/data/sign.lean

Modified src/dynamics/ergodic/add_circle.lean

Modified src/number_theory/zsqrtd/gaussian_int.lean

added theorem gaussian_int.abs_coe_nat_norm

deleted theorem gaussian_int.coe_nat_abs_norm

Modified src/ring_theory/int/basic.lean

added theorem int.abs_eq_normalize

deleted theorem int.coe_nat_abs_eq_normalize

deleted theorem int.normalize_of_neg

added theorem int.normalize_of_nonpos

Modified src/testing/slim_check/sampleable.lean