LinearAlgebra.Prod !4#2415

Stream: mathlib4

[Johan Commelin]

theorem prodMap_comp (f₁₂ : M →ₗ[R] M₂) (f₂₃ : M₂ →ₗ[R] M₃) (g₁₂ : M₄ →ₗ[R] M₅)
    (g₂₃ : M₅ →ₗ[R] M₆) :
    f₂₃.prodMap g₂₃ ∘ₗ f₁₂.prodMap g₁₂ = (f₂₃ ∘ₗ f₁₂).prodMap (g₂₃ ∘ₗ g₁₂) :=
  rfl

gives me

Prod.lean:347:4
unknown identifier 'include✝'
Prod.lean:347:4
unknown constant 'σ₁₃✝'
Prod.lean:347:42
unknown identifier 'include✝'
Prod.lean:347:42
unknown constant 'σ₁₃✝'

[Johan Commelin]

The only other error in the files is with

@[simp, norm_cast]
theorem coe_prod :
    (e₁.prod e₂ : M × M₃ →ₗ[R] M₂ × M₄) = (e₁ : M →ₗ[R] M₂).prodMap (e₂ : M₃ →ₗ[R] M₄) :=
  rfl

complaining

norm_cast: badly shaped lemma, lhs must contain at least one coe
  (LinearEquiv.prod e₁ e₂).toLinearMap

[Mario Carneiro]

is there an include in the file?

[Mario Carneiro]

perhaps after the theorem

[Johan Commelin]

include is an error in Lean 4, right?

[Mario Carneiro]

it's not a keyword, so it gets interpreted as an (unknown) identifier

[Johan Commelin]

https://github.com/leanprover-community/mathlib4/pull/2415/files says that there is no include

[Mario Carneiro]

CI also says that there is no error in the file

[Mario Carneiro]

there is an include σ₁₃ on line 560 of Algebra.Module.LinearMap

[Johan Commelin]

aha!

[Mario Carneiro]

Aha more:

infixr:80 " ∘ₗ " =>
  @LinearMap.comp _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ (RingHom.id _) (RingHom.id _) (RingHom.id _)
    RingHomCompTriple.ids

include σ₁₃

it's accidentally in the infix

[Mario Carneiro]

so you don't get the error unless you use ∘ₗ

[Mario Carneiro]

aha even more:

-- mathport name: «expr ∘ₗ »
set_option quotPrecheck false in -- Porting note: error message suggested to do this
/-- `∘ₗ` is notation for composition of two linear (not semilinear!) maps into a linear map.
This is useful when Lean is struggling to infer the `RingHomCompTriple` instance. -/
infixr:80 " ∘ₗ " =>
  @LinearMap.comp _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ (RingHom.id _) (RingHom.id _) (RingHom.id _)
    RingHomCompTriple.ids

include σ₁₃

normally this would be an error, but it has been suppressed by what appears to be a confused porter

[Johan Commelin]

oof, thanks for debugging!

[Johan Commelin]

This "include" issue is now fixed.

[Johan Commelin]

So this is the only error that is left

@[simp, norm_cast]
theorem coe_prod :
    (e₁.prod e₂ : M × M₃ →ₗ[R] M₂ × M₄) = (e₁ : M →ₗ[R] M₂).prodMap (e₂ : M₃ →ₗ[R] M₄) :=
  rfl

complaining

norm_cast: badly shaped lemma, lhs must contain at least one coe
  (LinearEquiv.prod e₁ e₂).toLinearMap

[Eric Wieser]

Is toLinearMap missing a @[coe] attribute?

[Johan Commelin]

Thanks! That fixes it!