Theorem Cardinal.mkRat

Modification history

2024-11-16 22:07

Mathlib/Data/Rat/Cardinal.lean

chore(Rat/Cardinal): reduce imports and create new file (#18584)

Modified Cardinal.mkRat View on Github →

2023-07-03 11:03

Mathlib/Data/Rat/Denumerable.lean

fix: precedence of `#` (#5623)

Modified Cardinal.mkRat View on Github →

2023-02-11 19:21

Mathlib/Data/Rat/Denumerable.lean

feat Port Data.Rat.Denumerable (#2197)

Added Cardinal.mkRat View on Github →