feat: port NumberTheory.LegendreSymbol.MulCharacter (#2994)

[Zulip thread](https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/!4.232994.20NumberTheory.2ELegendreSymbol.2EMulCharacter)



Co-authored-by: Parcly Taxel <reddeloostw@gmail.com>
Co-authored-by: int-y1 <jason_yuen2007@hotmail.com>
Co-authored-by: adomani <adomani@gmail.com>
Co-authored-by: damiano <adomani@gmail.com>

Mathlib.lean

@@ -1668,6 +1668,7 @@ import Mathlib.NumberTheory.ClassNumber.AdmissibleAbsoluteValue
 import Mathlib.NumberTheory.Divisors
 import Mathlib.NumberTheory.Fermat4
 import Mathlib.NumberTheory.FrobeniusNumber
+import Mathlib.NumberTheory.LegendreSymbol.MulCharacter
 import Mathlib.NumberTheory.LucasLehmer
 import Mathlib.NumberTheory.LucasPrimality
 import Mathlib.NumberTheory.Multiplicity

Mathlib/Data/MvPolynomial/Supported.lean

@@ -60,15 +60,15 @@ noncomputable def supportedEquivMvPolynomial (s : Set σ) : supported R s ≃ₐ
     (AlgEquiv.ofInjective (rename ((↑) : s → σ)) (rename_injective _ Subtype.val_injective)).symm
 #align mv_polynomial.supported_equiv_mv_polynomial MvPolynomial.supportedEquivMvPolynomial
 
-@[simp]
+@[simp, nolint simpNF]  -- porting note: the `simpNF` linter complained about this lemma.
 theorem supportedEquivMvPolynomial_symm_C (s : Set σ) (x : R) :
     (supportedEquivMvPolynomial s).symm (C x) = algebraMap R (supported R s) x := by
   ext1
   simp [supportedEquivMvPolynomial, MvPolynomial.algebraMap_eq]
 set_option linter.uppercaseLean3 false in
 #align mv_polynomial.supported_equiv_mv_polynomial_symm_C MvPolynomial.supportedEquivMvPolynomial_symm_C
 
-@[simp]
+@[simp, nolint simpNF]  -- porting note: the `simpNF` linter complained about this lemma.
 theorem supportedEquivMvPolynomial_symm_X (s : Set σ) (i : s) :
     (↑((supportedEquivMvPolynomial s).symm (X i : MvPolynomial s R)) : MvPolynomial σ R) = X ↑i :=
   by simp [supportedEquivMvPolynomial]