aboutsummaryrefslogtreecommitdiff
path: root/mathcomp/Make
diff options
context:
space:
mode:
authorCyril Cohen2017-12-12 20:01:11 +0100
committerCyril Cohen2017-12-14 13:22:31 +0100
commitc6e4012ec499b100abfd19320b6790d9849eba9e (patch)
treeb1d361fbd85bcd474d9fd6a937297f25a8aa36aa /mathcomp/Make
parent3e0f4874ce1d421e6a65eb8e745c666cb0313373 (diff)
The spaces generated by some delta_mx are in a direct sum
proof by @ggonthier
Diffstat (limited to 'mathcomp/Make')
0 files changed, 0 insertions, 0 deletions