Commit 2024-05-05 18:04 6821ad22

View on Github →

feat: more NNRat lemmas (#12586) Note that the previous version of Rat.ofScientific_eq_ofScientific was not well-formed, as it did not include the necessary ofNats.

Estimated changes

Modified Mathlib/Algebra/Field/Defs.lean

modified theorem Rat.ofScientific_eq_ofScientific

Modified Mathlib/Data/NNRat/Defs.lean

modified theorem NNRat.coe_pow

added theorem NNRat.den_ofNat

added theorem NNRat.num_ofNat

Modified Mathlib/Data/Rat/Cast/Lemmas.lean

added theorem NNRat.Nonneg.coe_ofScientific

added theorem NNRat.cast_pow

added theorem NNRat.cast_zpow_of_ne_zero

deleted theorem Nonneg.coe_ofScientific

Modified Mathlib/Data/Rat/Field.lean

added theorem NNRat.den_inv_of_ne_zero

added theorem NNRat.num_inv_of_ne_zero