mathlib3
c444a005 - Revert "chore(ring_theory): delete `is_algebra_tower`"

Commit

5 years ago

Revert "chore(ring_theory): delete `is_algebra_tower`" This reverts commit c956ce1516ccfb3139ae3ebde7ede9c678d81968.

Author

Vierkantor

Parents