LinearAlgebra.Span !4#2248

Stream: mathlib4

[Johan Commelin]

def toSpanNonzeroSingleton (x : V) (h : x ≠ 0) : K ≃ₗ[K] K ∙ x := -- error on the type
-- failed to synthesize instance
--   RingHomInvPair (RingHom.id K) ?m.479207

[Johan Commelin]

Adding an instance RingHomInvPair (RingHom.id K) (RingHom.id K) doesn't even help.

[Eric Wieser]

What does it want with pp.explicit true?

[Eric Wieser]

This is surely still the typeclass eta bug

[Johan Commelin]

failed to synthesize instance
  @RingHomInvPair K K (@DivisionSemiring.toSemiring K (@Semifield.toDivisionSemiring K (@Field.toSemifield K inst✝²)))
    (@DivisionSemiring.toSemiring K (@Semifield.toDivisionSemiring K (@Field.toSemifield K inst✝²)))
    (@RingHom.id K
      (@NonAssocRing.toNonAssocSemiring K
        (@Ring.toNonAssocRing K (@DivisionRing.toRing K (@Field.toDivisionRing K inst✝²)))))
    ?m.479207

[Johan Commelin]

Aha, I see NonAssocRing. So maybe the fix that @Pol'tta / Kô Miyahara found will work here as well

[Johan Commelin]

Yep, that helps!

[Johan Commelin]

file is now error-free

[Eric Wieser]

Do you remember the issue number I'm thinking of?

[Johan Commelin]

lean4#2074 ?