mathlib
f03f5a96 - feat(ring_theory/algebra_tower): Restriction of adjoin (#5767)

Commit

5 years ago

feat(ring_theory/algebra_tower): Restriction of adjoin (#5767) Two technical lemmas about restricting `algebra.adjoin` within an `is_scalar_tower`.

Author

tb65536

Parents