duplicate lemmas

Stream: mathlib4

[Johan Commelin]

docs#LinearMap.toMatrix_apply' seems to be a verbatim duplicate of docs#LinearMap.toMatrix_apply
Does anyone know if I'm missing something, or whether there was an intended difference in the past?

[Riccardo Brasca]

I don't know why we have both, but I agree they look exactly the same.

[Riccardo Brasca]

import Mathlib.LinearAlgebra.Matrix.ToLin

example : @LinearMap.toMatrix_apply = @LinearMap.toMatrix_apply' := rfl

confirms this.

[Eric Wieser]

Strictly you should use by with_reducible rfl to test that

[Eric Wieser]

Were they different in Lean 3?

[Kevin Buzzard]

That check would also not check binder types, right?

[Riccardo Brasca]

They're identical in the latest mathlib3

[Riccardo Brasca]

I think it's just an accident, introduced in mathlib#4345