Theorem Units.embed_product_star

Modification history

2023-08-31 08:18
Mathlib/Algebra/Star/Prod.lean
refactor(Algebra/Star/*): Allow for star operation on non-associative algebras (#6562) …
Modified Units.embed_product_starView on Github →
2023-01-09 14:13
Mathlib/Algebra/Star/Prod.lean
feat: port Algebra.Star.Prod (#1434)
Added Units.embed_product_starView on Github →