Commit 2024-11-16 22:07 a0cd3d6f

View on Github →

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

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Rat/Cardinal.lean

added theorem Cardinal.mkRat

Modified Mathlib/Data/Rat/Denumerable.lean

deleted theorem Cardinal.mkRat

Modified Mathlib/Data/Real/Cardinality.lean

Modified Mathlib/FieldTheory/Cardinality.lean

Modified Mathlib/ModelTheory/Order.lean