to_matrix change

Stream: general

[orlando]

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]

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

[Jalex Stark]

does this help?

import data.matrix.pequiv
#check pequiv.to_matrix

[Yury G. Kudryashov]

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

[Kevin Buzzard]

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]

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

i will see tomorrow :confused:

[Reid Barton]

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

[orlando]

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

[Johan Commelin]

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

[orlando]

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]

:grinning_face_with_smiling_eyes: :grinning_face_with_smiling_eyes: :grinning_face_with_smiling_eyes:

[Yury G. Kudryashov]

2.gcd 5 looks funny too.

[Yury G. Kudryashov]

But you can change this option locally.

[Yury G. Kudryashov]

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

[orlando]

@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]

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

[Patrick Massot]

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]

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