Theorem coe_mul_coe

Modification history

2024-11-28 16:50
Mathlib/Algebra/Group/Subgroup/Pointwise.lean
feat: `S ^ n = S` where `S` is a submonoid (#19259) …
Modified coe_mul_coeView on Github →
2024-02-29 21:30
Mathlib/GroupTheory/Subgroup/Pointwise.lean
feat: `IsTorsionFree M ↔ NoZeroSMulDivisors ℕ M` (#10918) …
Added coe_mul_coeView on Github →