Commit 2023-08-04 18:54 90907eb3

View on Github →

feat(SetTheory/Cardinal): add ofNat lemmas (#6362)

Estimated changes

Modified Mathlib/LinearAlgebra/Finrank.lean

added theorem FiniteDimensional.rank_eq_ofNat_iff_finrank_eq_ofNat

added theorem FiniteDimensional.rank_eq_one_iff_finrank_eq_one

Modified Mathlib/SetTheory/Cardinal/Basic.lean

added theorem Cardinal.toNat_eq_ofNat

Modified Mathlib/SetTheory/Cardinal/Finite.lean