Mathlib Changelog
v4
Changelog
About
Github
Commit
2023-02-21 10:05
d9fac07d
View on Github →
feat: port Algebra.Algebra.Prod (
#2383
)
Estimated changes
Modified
Mathlib.lean
Created
Mathlib/Algebra/Algebra/Prod.lean
added
theorem
AlgHom.coe_prod
added
def
AlgHom.fst
added
theorem
AlgHom.fst_prod
added
def
AlgHom.prod
added
def
AlgHom.prodEquiv
added
theorem
AlgHom.prod_fst_snd
added
def
AlgHom.snd
added
theorem
AlgHom.snd_prod
added
theorem
Prod.algebraMap_apply