Theorems · Theorem · number theory
MulChar.map_zero
∀ {R' : Type u_2} [inst : CommMonoidWithZero R'] {R : Type u_3} [inst_1 : CommMonoidWithZero R] [Nontrivial R]
(χ : MulChar R R'), χ 0 = 0If the domain has a zero (and is nontrivial), then χ 0 = 0.
- Defined in
- Mathlib.NumberTheory.MulChar.Basic
- Cited by
- 10 results in Mathlib
- Foundations
- Depth 15 from the axioms · uses Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement · cited by 62,936
- Nontrivialstatement and proof · cited by 2,416
- CommMonoidWithZerostatement and proof · cited by 913
- MulCharstatement and proof · cited by 186
- not_isUnit_zeroproof · cited by 20
- MulChar.map_nonunitproof · cited by 13
Cited by11
Results whose statement or proof uses this declaration.
- quadraticChar_neg_one_iff_not_isSquareproof · cited by 4
- DirichletCharacter.map_zero'proof · cited by 3
- jacobiSum_mul_nontrivialproof · cited by 3
- MulChar.inv_applyproof · cited by 2
- MulChar.apply_mem_algebraAdjoin_of_pow_eq_oneproof · cited by 2
- jacobiSum_eq_sum_sdiffproof · cited by 1
- MulChar.toMonoidWithZeroHomproof · cited by 1
- quadraticChar_card_sqrtsproof · cited by 1
- jacobiSum_nontrivial_invproof · cited by 0
- legendreSym.at_zeroproof · cited by 0
- MulChar.map_ringCharproof · cited by 0