Theorem MulAction.Quotient.coe_smul_out

Modification history

2025-01-16 11:16
Mathlib/GroupTheory/GroupAction/Quotient.lean
chore: survey of simp porting notes (#20787) …
Modified MulAction.Quotient.coe_smul_outView on Github →
2024-11-20 14:09
Mathlib/GroupTheory/GroupAction/Quotient.lean
chore: deprecate `Quotient.out'` (#17941)
Added MulAction.Quotient.coe_smul_outView on Github →