diff options
| author | Cyril Cohen | 2017-12-12 20:01:11 +0100 |
|---|---|---|
| committer | Cyril Cohen | 2017-12-14 13:22:31 +0100 |
| commit | c6e4012ec499b100abfd19320b6790d9849eba9e (patch) | |
| tree | b1d361fbd85bcd474d9fd6a937297f25a8aa36aa /mathcomp/_CoqProject | |
| parent | 3e0f4874ce1d421e6a65eb8e745c666cb0313373 (diff) | |
The spaces generated by some delta_mx are in a direct sum
proof by @ggonthier
Diffstat (limited to 'mathcomp/_CoqProject')
0 files changed, 0 insertions, 0 deletions