Lean: semi-invariants of a finite group via linearIndependent_monoidHom

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.