Theorem Subgroup.mem_inv_pointwise_smul_iff₀

Modification history

2025-04-09 09:39

Mathlib/Algebra/Group/Subgroup/Pointwise.lean

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

Modified Subgroup.mem_inv_pointwise_smul_iff₀ View on Github →

2023-02-01 11:22

Mathlib/GroupTheory/Subgroup/Pointwise.lean

feat: port GroupTheory.Subgroup.Pointwise (#1981)

Added Subgroup.mem_inv_pointwise_smul_iff₀ View on Github →