feat(NumberTheory/LegendreSymbol/MulCharacter): weaken assumptions (#…

…11012)

This PR weakens the type class assumptions on some results about multiplicative characters  (from assuming the domain is a commutative ring to only requiring it is a commutative monoid).

See [here](https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/Multiplicative.20characters.20of.20finite.20groups/near/423605701) on Zulip.



Co-authored-by: Michael Stoll <99838730+MichaelStollBayreuth@users.noreply.github.com>

Mathlib/NumberTheory/LegendreSymbol/MulCharacter.lean

@@ -419,7 +419,7 @@ end DefinitionAndGroup
 We introduce the properties of being nontrivial or quadratic and prove
 some basic facts about them.
 
-We now assume that domain and target are commutative rings.
+We now (mostly) assume that the target is a commutative ring.
 -/
 
 
@@ -429,7 +429,9 @@ namespace MulChar
 
 universe u v w
 
-variable {R : Type u} [CommRing R] {R' : Type v} [CommRing R'] {R'' : Type w} [CommRing R'']
+section nontrivial
+
+variable {R : Type u} [CommMonoid R] {R' : Type v} [CommMonoidWithZero R']
 
 /-- A multiplicative character is *nontrivial* if it takes a value `≠ 1` on a unit. -/
 def IsNontrivial (χ : MulChar R R') : Prop :=
@@ -441,6 +443,12 @@ theorem isNontrivial_iff (χ : MulChar R R') : χ.IsNontrivial ↔ χ ≠ 1 := b
   simp only [IsNontrivial, Ne.def, ext_iff, not_forall, one_apply_coe]
 #align mul_char.is_nontrivial_iff MulChar.isNontrivial_iff
 
+end nontrivial
+
+section quadratic_and_comp
+
+variable {R : Type u} [CommMonoid R] {R' : Type v} [CommRing R'] {R'' : Type w} [CommRing R'']
+
 /-- A multiplicative character is *quadratic* if it takes only the values `0`, `1`, `-1`. -/
 def IsQuadratic (χ : MulChar R R') : Prop :=
   ∀ a, χ a = 0 ∨ χ a = 1 ∨ χ a = -1
@@ -522,11 +530,17 @@ theorem IsQuadratic.pow_odd {χ : MulChar R R'} (hχ : χ.IsQuadratic) {n : ℕ}
   rw [pow_add, pow_one, hχ.pow_even (even_two_mul _), one_mul]
 #align mul_char.is_quadratic.pow_odd MulChar.IsQuadratic.pow_odd
 
+end quadratic_and_comp
+
 open BigOperators
 
+section sum
+
+variable {R : Type u} [CommMonoid R] [Fintype R] {R' : Type v} [CommRing R']
+
 /-- The sum over all values of a nontrivial multiplicative character on a finite ring is zero
 (when the target is a domain). -/
-theorem IsNontrivial.sum_eq_zero [Fintype R] [IsDomain R'] {χ : MulChar R R'}
+theorem IsNontrivial.sum_eq_zero [IsDomain R'] {χ : MulChar R R'}
     (hχ : χ.IsNontrivial) : ∑ a, χ a = 0 := by
   rcases hχ with ⟨b, hb⟩
   refine' eq_zero_of_mul_eq_self_left hb _
@@ -554,6 +568,8 @@ theorem sum_one_eq_card_units [Fintype R] [DecidableEq R] :
       Function.Embedding.coeFn_mk, exists_true_left, IsUnit]
 #align mul_char.sum_one_eq_card_units MulChar.sum_one_eq_card_units
 
+end sum
+
 end MulChar
 
 end Properties