Module on hamming

Stream: general

[Bolton Bailey]

@Wrenna Robson you asked about this. This is a MWE for hamming not getting a module typeclass. Why doesn't the instance docs#hamming.module fire here?

import information_theory.hamming
import linear_algebra.finite_dimensional

def linear_code (𝓓 F : Type) [fintype 𝓓] [field F] := submodule F (hamming ( λ d : 𝓓, F ))

variables {𝓓 F : Type} [fintype 𝓓] [field F]

noncomputable def dimension (C : linear_code 𝓓 F) : ℕ :=
set.finrank F C.carrier

[Wrenna Robson]

This is a good question. It does with the type synonym, I assume?

[Wrenna Robson]

Does it if you spell that D -> F (with the proper unicode)?

[Bolton Bailey]

Yes, that works fine

[Eric Wieser]

This looks like the standard dependent typeclass issue that we have all the time with pi types

[Eric Wieser]

Lean isn't always able to conclude that @module R M ring.to_semiring _ is the same type as @module R M comm_semiring.to_semiring _

[Eric Wieser]

In particular, it frequently fails to do so in the presence of pi types