mathlib3
c7bce281 - feat(field_theory/tower): generalize `rank_mul_rank` to rings (#18885)

Commit

2 years ago

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

Author

eric-wieser

Parents