Mathlib v3 is deprecated. Go to Mathlib v4

Theorem add_submonoid.coe_pointwise_smul

Modification history

2021-09-24 21:40
src/group_theory/submonoid/pointwise.lean
feat(group_theory/*/pointwise): Copy set lemmas about pointwise actions to subgroups and submonoids (#9359) …
Modified add_submonoid.coe_pointwise_smulView on Github →
2021-09-20 11:48
src/group_theory/submonoid/operations.lean
chore(group_theory/submonoid/operations): split a file (#9292)
Modified add_submonoid.coe_pointwise_smulView on Github →
2021-09-09 14:10
src/group_theory/submonoid/operations.lean
feat(group_theory/sub{monoid,group}): pointwise actions on `add_sub{monoid,group}`s and `sub{monoid,group,module,semiring,ring,algebra}`s (#8945) …
Added add_submonoid.coe_pointwise_smulView on Github →