Commit 2023-01-09 14:13 ef529d52

View on Github →

feat: port Algebra.Star.Prod (#1434)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Star/Prod.lean

added theorem Prod.fst_star

added theorem Prod.snd_star

added theorem Prod.star_def

added theorem Units.embed_product_star