Theorem FractionalIdeal.coe_natCast

Modification history

2026-09-20 11:52
Mathlib/RingTheory/FractionalIdeal/Basic.lean
style: fix a few instances of 'leading by' (#43995) …
Modified FractionalIdeal.coe_natCastView on Github →
2024-04-17 11:15
Mathlib/RingTheory/FractionalIdeal/Basic.lean
chore: Rename `nat_cast`/`int_cast`/`rat_cast` to `natCast`/`intCast`/`ratCast` (#11486) …
Added FractionalIdeal.coe_natCastView on Github →