Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-04-28 14:14 c7bce281

View on Github →

feat(field_theory/tower): generalize rank_mul_rank to rings (#18885) This also renames rank_mul_rank to lift_rank_mul_lift_rank

Estimated changes

Modified src/data/complex/module.lean

Modified src/field_theory/tower.lean

added theorem finite_dimensional.finrank_mul_finrank'

modified theorem finite_dimensional.finrank_mul_finrank

added theorem lift_rank_mul_lift_rank

deleted theorem rank_mul_rank'

modified theorem rank_mul_rank