Commit 2021-11-01 11:06 9ef310f2

View on Github →

chore(algebra/algebra): implement subalgebra.under in terms of restrict_scalars (#10080) We should probably remove subalgebra.under entirely, but that's likely a lot more work.

Estimated changes

Modified src/algebra/algebra/subalgebra.lean

deleted theorem subalgebra.mem_under

deleted def subalgebra.under

Modified src/algebra/algebra/tower.lean

added theorem subalgebra.mem_under

added def subalgebra.under

Modified src/ring_theory/adjoin/basic.lean

modified theorem algebra.adjoin_induction