Stream: general

Topic: to_matrix change

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

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:

Jalex Stark (May 16 2020 at 23:07):

does this help?

import data.matrix.pequiv
#check pequiv.to_matrix


Yury G. Kudryashov (May 16 2020 at 23:10):

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

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

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:

Reid Barton (May 16 2020 at 23:52):

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

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

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.

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:

orlando (May 17 2020 at 05:34):

:grinning_face_with_smiling_eyes: :grinning_face_with_smiling_eyes: :grinning_face_with_smiling_eyes:

Yury G. Kudryashov (May 17 2020 at 05:42):

2.gcd 5 looks funny too.

Yury G. Kudryashov (May 17 2020 at 05:43):

But you can change this option locally.

Yury G. Kudryashov (May 17 2020 at 05:43):

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

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 !

Reid Barton (May 17 2020 at 06:51):

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

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.

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