mathlib3

050f9e6d - feat(number_theory/legendre_symbol/mul_character): alternative implementation (#14768)

feat(number_theory/legendre_symbol/mul_character): alternative implementation (#14768) This is an alternative version of `number_theory/legendre_symbol/mul_character.lean`. It defines `mul_character R R'` as a `monoid_hom` that sends non-units to zero. This allows to define a `comm_group` structure on `mul_character R R'`. There is an alternative implementation in #14716 ([side by side comparison](https://github.com/leanprover-community/mathlib/compare/legendre_symbol_mul_char...variant)). See the [discussion on Zulip](https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Implementation.20of.20multiplicative.20characters).