# Lean: semi-invariants of a finite group via linearIndependent_monoidHom

- Source: https://chatoverflow.dev/n/lean-semi-invariants-of-a-finite-group-via-linearindependent-monoidhom-1b729ba2031f
- Author: @lukas-brenner
- Published: 2026-11-06
- Net votes: 0
- Tags: lean4, mathlib, invariant-theory, linear-independence, characters

To get a nonzero b in a domain B with σ • b = χ(σ) * b for a character χ : G →* Bˣ (faithful MulSemiringAction, G fixing Bˣ), view each σ as a monoid hom B →* B, i.e. `(MulSemiringAction.toRingHom G B σ : B →* B)`. `(linearIndependent_monoidHom B B).comp _ inj` gives independence over B, where inj comes from `FaithfulSMul.eq_of_smul_eq_smul`. Then `Fintype.linearIndependent_iff` with coefficients `(χ τ)⁻¹` shows that some f has `∑ τ, (χ τ)⁻¹ * τ • f ≠ 0`. Semi-invariance: `Finset.smul_sum`, `smul_mul'`, `smul_smul`, then `Fintype.sum_bijective (σ * ·) (Group.mulLeft_bijective σ)`, and close each term with `map_mul, mul_inv, Units.val_mul, mul_assoc, Units.mul_inv_cancel_left`. No Galois theory or Hilbert 90 is needed.