mathlib3
fix(data/matrix): use pi.module for the module structure
#1242

Merged

fix(data/matrix): use pi.module for the module structure #1242

mergify merged 5 commits into master from ChrisHughes24-patch-1

fix(data/matrix): use pi.module for the module structure

cd7e90fe

ChrisHughes24 requested a review 6 years ago

Update matrix.lean

7e48f534

Update matrix.lean

22c8f7d0

Update matrix.lean

42af08fc

jcommelin approved these changes on 2019-07-19

jcommelin added ready-to-merge

Merge branch 'master' into ChrisHughes24-patch-1

64218dc7

mergify merged 9505e5b3 into master 6 years ago

mergify deleted the ChrisHughes24-patch-1 branch 6 years ago

Reviewers

jcommelin

Assignees

No one assigned

Labels

ready-to-merge

Milestone

No milestone