Zulip Chat Archive

Stream: general

Topic: to_matrix change


view this post on Zulip orlando (May 16 2020 at 22:35):

Hello,

I little question, i upgrate mathlib and the notation in tactic state for to_matrix change !

So the change is f.to_matrix instead of to_matrix f can i do something to have the to_matrix f ? thx

view this post on Zulip orlando (May 16 2020 at 22:37):

ohhh it's also for range f and ker f now it's f.ker and f.range :scream:

view this post on Zulip Jalex Stark (May 16 2020 at 23:07):

does this help?

import data.matrix.pequiv
#check pequiv.to_matrix

view this post on Zulip Yury G. Kudryashov (May 16 2020 at 23:10):

Some option about pretty printing changed its default value. Look at recently closed lean PRs

view this post on Zulip Kevin Buzzard (May 16 2020 at 23:15):

It's really hard to understand lean changes by just looking at old PRs if you are not one of the people who spends a lot of time looking at lean PRs

view this post on Zulip orlando (May 16 2020 at 23:21):

@Jalex Stark : hum no it's linear_map.to_matrix define in the file linear algebra. matrix !

i will see tomorrow :confused:

view this post on Zulip Reid Barton (May 16 2020 at 23:52):

set_option pp.generalized_field_notation false (the default changed to true)

view this post on Zulip orlando (May 17 2020 at 04:48):

:+1: :+1: :+1:

view this post on Zulip Johan Commelin (May 17 2020 at 05:20):

@orlando In particular, nothing really changed. Only the way code was displayed in the tactic state. The entire mathlib code stayed the same.

view this post on Zulip orlando (May 17 2020 at 05:34):

Yes @Johan Commelin it's just the tactic display, but that stress me a lot

x  ker (f^10+ 147* f^15 + 4566 f^10000+f^795)

:+1:

 ((f^10+ 147* f^15 + 4566 f^10000+f^795).rek  \ni  x

:+1:

x   ((f^10+ 147* f^15 + 4566 f^10000+f^795).ker

:-1:

view this post on Zulip orlando (May 17 2020 at 05:34):

:grinning_face_with_smiling_eyes: :grinning_face_with_smiling_eyes: :grinning_face_with_smiling_eyes:

view this post on Zulip Yury G. Kudryashov (May 17 2020 at 05:42):

2.gcd 5 looks funny too.

view this post on Zulip Yury G. Kudryashov (May 17 2020 at 05:43):

But you can change this option locally.

view this post on Zulip Yury G. Kudryashov (May 17 2020 at 05:43):

I often use protected definitions with long namespace names, and I like the new way.

view this post on Zulip orlando (May 17 2020 at 05:58):

@Yury G. Kudryashov : in the expression
x ∈ ((f^10+ 147* f^15 + 4566 f^10000+f^795).ker
My problem is x ∈ ((f^10+ 147* f^15 + 4566 f^10000+f^795). doesn't make sense and You have to go look far to the right to see that the right member of the formule _ ∈ _ is a module.

When you see x ∈ ker (... ) the Typage is directly ok ! ( my english is bad :upside_down: ). it's maybe it's a lack of habit. But I am very sensitive to the notation. For example, the big operator file became much clearer for me with the mathematical notation. Before I understood absolutely nothing at all !

view this post on Zulip Reid Barton (May 17 2020 at 06:51):

Maybe it shouldn't apply to open namespaces? Though I could imagine that getting confusing perhaps...

view this post on Zulip Patrick Massot (May 17 2020 at 09:59):

I agree with Orlando that x ∈ f.ker is really bad. I love dot notation in general, but that one is clearly going in the wrong direction.

view this post on Zulip Reid Barton (May 17 2020 at 10:02):

I wonder if you can also fix it with something like notation `ker` := ker.


Last updated: May 11 2021 at 02:05 UTC