!4#3354 (LinearAlgebra.Dimension)

Stream: PR reviews

[Jeremy Tan]

Most of the remaining errors deal with Module.rank and using it to definitionally simplify (as in dsimp [Module.rank])

[Jeremy Tan]

In the very first theorem lift_dim_le_of_injective, after dsimp [Module.rank] the goal state in Lean 3 is

(⨆ (ι : {s // linear_independent R coe}), #↥↑ι).lift ≤
    (⨆ (ι : {s // linear_independent R coe}), #↥↑ι).lift

but in Lean 4 it is the very strange

lift (Wrapper.value✝ wrapped✝ R M) ≤ lift (Wrapper.value✝ wrapped✝ R M')

It may have something to do with the use of the up-arrow to replace the coe in Lean 3. Is there something wrong with the up-arrow replacement I've made in the Lean 4 definition?

protected irreducible_def Module.rank : Cardinal :=
  ⨆ ι : { s : Set V // LinearIndependent K ((↑) : s → V) }, #ι.1

[Notification Bot]

2 messages were moved here from #PR reviews > !4#3247 by Jeremy Tan.

[Jeremy Tan]

…right, @Pol'tta / Kô Miyahara got there first while I was opening a sync PR

[Eric Wieser]

(!4#3354)

[Scott Morrison]

Merged again!

[Eric Wieser]

@Jeremy Tan, for future reference it's best to restart with new mathport output (re-run start_port and rebase your changes onto the resulting commit) if you realize you started with the wrong mathport output