Commit 2022-12-16 11:44 07ab3cf7

View on Github →

feat: Port GroupTheory.GroupAction.Prod (#1056) mathlib3 SHA: aba57d4d3dae35460225919dcd82fe91355162f9

Estimated changes

added theorem Prod.pow_def
added theorem Prod.pow_fst
added theorem Prod.pow_mk
added theorem Prod.pow_snd
added theorem Prod.pow_swap
added theorem Prod.smul_def
added theorem Prod.smul_fst
added theorem Prod.smul_mk
added theorem Prod.smul_mk_zero
added theorem Prod.smul_snd
added theorem Prod.smul_swap
added theorem Prod.smul_zero_mk
added def smulMonoidHom
added def smulMulHom