Commit 2024-05-16 09:18 837a98af

View on Github →

feat: natCast versions of some Rat.intCast lemmas (#12814) also some golf

Estimated changes

Modified Mathlib/Data/Rat/Defs.lean

added theorem Rat.natCast_div_eq_divInt

Modified Mathlib/Data/Rat/Lemmas.lean

deleted theorem Rat.den_div_cast_eq_one_iff

added theorem Rat.den_div_intCast_eq_one_iff

added theorem Rat.den_div_natCast_eq_one_iff

modified theorem Rat.natCast_div

Modified Mathlib/RingTheory/WittVector/StructurePolynomial.lean