Theorem NNRatCast.ofScientific_eq_ite

Modification history

2026-06-10 19:34

Mathlib/Algebra/Field/Rat.lean

feat(Tactic): generalize ofScientific NormNum extension to `DivisionSemiring` (#34805)

Added NNRatCast.ofScientific_eq_ite View on Github →