Commit 2020-12-16 21:52 8fa10afc

View on Github →

feat(ring_theory/algebra_tower): alg_hom_equiv_sigma (#5345) Proves that algebra homomorphisms from the top of an is_scalar_tower are the same as a pair of algebra homomorphisms. This is useful for counting algebra homomorphisms.

Estimated changes

Modified src/ring_theory/algebra_tower.lean

added def alg_hom.extend_scalars

added def alg_hom.restrict_domain

added def alg_hom_equiv_sigma