Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-18 15:45 d790b4b8

View on Github →

feat(set_theory/cardinal): lt_omega_of_fintype (#13365)

Estimated changes

Modified archive/100-theorems-list/82_cubing_a_cube.lean

Modified src/data/W/cardinal.lean

Modified src/data/mv_polynomial/cardinal.lean

Modified src/data/polynomial/cardinal.lean

Modified src/field_theory/is_alg_closed/classification.lean

Modified src/linear_algebra/finsupp_vector_space.lean

Modified src/set_theory/cardinal.lean

added theorem cardinal.lt_omega_of_fintype