Commit 2025-01-25 06:17 98e59552

View on Github →

feat(Algebra/Algebra/Prod): simple theorems about fst, snd and prod (#21020) Very basic theorems about AlgHom.fst, AlgHom.snd and AlgHom.prod. Counterparts for LinearMap already exist.

Estimated changes

added theorem AlgHom.fst_apply
added theorem AlgHom.prod_comp
modified theorem AlgHom.prod_fst_snd
added theorem AlgHom.snd_apply