Commit 2021-11-26 16:20 dabb58bb

View on Github →

chore(algebra/module/pi): split out group_theory/group_action/pi to match group_theory/group_action/prod (#10485) These declarations are copied without modification.

Estimated changes

Modified src/algebra/module/pi.lean

deleted theorem function.extend_smul

deleted theorem function.update_smul

deleted theorem pi.has_faithful_scalar_at

deleted theorem pi.single_smul'

deleted theorem pi.single_smul

deleted theorem pi.single_smul₀

deleted theorem pi.smul_apply'

deleted theorem pi.smul_apply

deleted theorem pi.smul_def

deleted theorem set.piecewise_smul

Modified src/data/fin/vec_notation.lean

Created src/group_theory/group_action/pi.lean

added theorem function.extend_smul

added theorem function.update_smul

added theorem pi.has_faithful_scalar_at

added theorem pi.single_smul'

added theorem pi.single_smul

added theorem pi.single_smul₀

added theorem pi.smul_apply'

added theorem pi.smul_apply

added theorem pi.smul_def

added theorem set.piecewise_smul