Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-25 06:24 feb9aed4

View on Github →

feat(group_theory/group_action/basic): More API for quotient_action (#13661) This PR adds a couple more API lemmas for quotient_action.

Estimated changes

Modified src/group_theory/group_action/basic.lean

added theorem mul_action.quotient.coe_smul_out'

added theorem mul_action.quotient.mk_smul_out'

modified theorem mul_action.quotient.smul_coe

modified theorem mul_action.quotient.smul_mk