Theorem NNRat.coe_one

Modification history

2024-06-20 09:54

Mathlib/Data/NNRat/Defs.lean

chore: remove unnecessary `nolint simpNF`s (#13982) …

Modified NNRat.coe_one View on Github →

2024-04-23 23:19

Mathlib/Data/NNRat/Defs.lean

feat: `NNRat.cast` (#11203) …

Modified NNRat.coe_one View on Github →

2023-02-21 07:40

Mathlib/Data/Rat/NNRat.lean

feat: port Data.Rat.NNRat (#2392)

Added NNRat.coe_one View on Github →