Stream: new members
Topic: Direct sum
Thomas Browning (Aug 18 2020 at 06:51):
I'm having trouble getting the direct sum notation to work.
import linear_algebra.direct_sum_module noncomputable theory local attribute [instance, priority 100] classical.prop_decidable open_locale direct_sum variables (E : Type*) [field E] (B : set E) example : B = B := begin have h := @direct_sum.semimodule E _ B _ (λ b, E) _ _, --have EB := (⊕ (b : B), (λ (x : B), E) b), --have EB := (⊕ (b : B), E), refl, end
Lean doesn't like either of these two attempts at defining EB (the direct sum of B copies of E).
Thomas Browning (Aug 18 2020 at 06:52):
The first attempt is a directly copy what lean tells me that h is
Kyle Miller (Aug 18 2020 at 06:54):
It's the wrong unicode character.
have EB := (⨁ (b : B), E),
(At least in emacs, it's
\O+ rather than
Thomas Browning (Aug 18 2020 at 06:55):
You're right. That was silly.
Kyle Miller (Aug 18 2020 at 06:55):
(I still get
Σ mixed up...)
Eric Wieser (Aug 18 2020 at 09:37):
Also silly is how vscode (at least, on windows) renders the n-ary
\O+ as smaller than the binary
Eric Wieser (Aug 18 2020 at 09:38):
Scott Morrison (Aug 18 2020 at 10:20):
You can select different fonts in VSCode. Often a font is missing some characters, so I think most people specify several, and VSCode falls back through the list.
I have "Menlo, Monaco, 'Courier New', monospace", but no particular reason to think this is good. (In particular I notice I'm missing the "subscript l" all throughout the linear algebra library, but never fixed it.)
Johan Commelin (Aug 18 2020 at 11:00):
DejaVu Sans Mono covers a lot
Last updated: May 09 2021 at 19:11 UTC