Def GradedModule.linearEquiv

Modification history

2023-10-19 13:16

Mathlib/Algebra/Module/GradedModule.lean

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

Modified GradedModule.linearEquiv View on Github →

2023-05-25 11:24

Mathlib/Algebra/Module/GradedModule.lean

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

Added GradedModule.linearEquiv View on Github →