Modifying Dedekind's linear independence of characters

Stream: mathlib4

[Xavier Xarles]

I would like to show in mathlib a generalized version of Dedekind's linear independence of characters using the same structure of the mathlib4 version, called linearIndependent_monoidHom. The difference is that instead of actual result

theorem linearIndependent_monoidHom (G : Type*) [Monoid G] (L : Type*) [CommRing L]
    [NoZeroDivisors L] : LinearIndependent L (M := G → L) (fun f => f : (G →* L) → G → L) := sorry

I want something like

import Mathlib.LinearAlgebra.LinearIndependent

theorem linearIndependent_mulHom (G : Type*) [Mul G] (L : Type*) [CommRing L]
    [NoZeroDivisors L] : LinearIndependent L (M := G → L) (fun f => f : (G →ₙ* L ) → G → L) := sorry

But, for the result to be true, I need to add the condition that the homs f should be non-zero (e.g. ∃ x, f x ≠ 0), I don't know how to do it with that format of the theorem. I am not asking for a proof of the result... just the statement.

[Eric Wieser]

This should work:

theorem linearIndependent_mulHom (G L : Type*) [Mul G] [CommRing L] [NoZeroDivisors L] :
    LinearIndependent L (· : {f : G →ₙ* L // ∃ x, f x ≠ 0} → G → L) :=
  sorry

[Eric Wieser]

The direct answer to your question is "add the condition by using a subtype"

[Eric Wieser]

fun f => f would still work instead of ·

[Xavier Xarles]

What it is the difference between writing {f : G →ₙ* L // ∃ x, f x ≠ 0} and {f : G →ₙ* L | ∃ x, f x ≠ 0} ? Because I don't understand how to "extract" from g:{f : G →ₙ* L // ∃ x, f x ≠ 0} the fact that ∃ x, g x ≠ 0 in the first case... (in the second I have g∈ {f : G →ₙ* L // ∃ x, f x ≠ 0}, which is a Proposition).

[Xavier Xarles]

I know that the first one is a subtype, and the second a subset.

[Ruben Van de Velde]

g.prop

[Xavier Xarles]

Aha, or g.2 also works...