Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-01-16 09:11 f03f5a96

View on Github →

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

Estimated changes

added theorem algebra.adjoin_res