mathlib3
c956ce15 - chore(ring_theory): delete `is_algebra_tower`

Commit
5 years ago
chore(ring_theory): delete `is_algebra_tower` Delete the abbreviation `is_algebra_tower` for `is_scalar_tower`, and replace all references (including the usages of the `is_algebra_tower` namespace) with `is_scalar_tower`. Documentation should also have been updated accordingly. This change was requested in a comment on #3717.
Author
Committer
Parents
Loading