Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-06-30 06:53 050f9e6d

View on Github →

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). See the discussion on Zulip.

Estimated changes

added theorem mul_char.coe_coe
added theorem mul_char.coe_mk
added theorem mul_char.ext'
added theorem mul_char.ext
added theorem mul_char.ext_iff
added def mul_char.inv
added theorem mul_char.inv_apply'
added theorem mul_char.inv_apply
added theorem mul_char.inv_mul
added theorem mul_char.map_nonunit
added theorem mul_char.map_one
added theorem mul_char.map_zero
added def mul_char.mul
added theorem mul_char.mul_apply
added theorem mul_char.mul_one
added theorem mul_char.one_apply_coe
added theorem mul_char.one_mul
added theorem mul_char.pow_apply'
added theorem mul_char.pow_apply_coe
added theorem mul_char.to_fun_eq_coe
added def mul_char.trivial
added structure mul_char