Theorem AddSubgroup.pointwise_smul_def

Modification history

2025-04-09 09:39

Mathlib/Algebra/Group/Subgroup/Pointwise.lean

chore(Algebra/Group/Subgroup/Pointwise): don't import `GroupWithZero` (#23832) …

Modified AddSubgroup.pointwise_smul_def View on Github →

2024-05-22 06:25

Mathlib/Algebra/Group/Subgroup/Pointwise.lean

Feat(Algebra/Group/Subgroup/Pointwise): Additive `Subgroup.pointwise_smul_def` (#13099) …

Added AddSubgroup.pointwise_smul_def View on Github →