Theorem DirectSum.Gmodule.smul_def

Modification history

2023-10-19 13:16

Mathlib/Algebra/Module/GradedModule.lean

feat(Algebra/Module/GradedModule): generalize `+` to `+ᵥ` in indicies (#7573) …

Modified DirectSum.Gmodule.smul_def View on Github →

2023-05-25 11:24

Mathlib/Algebra/Module/GradedModule.lean

feat: port Algebra.Module.GradedModule (#4228) …

Added DirectSum.Gmodule.smul_def View on Github →