Theorems · Theorem · number theory
MulChar.equivToUnitHom_symm_coe
∀ {R : Type u_1} [inst : CommMonoid R] {R' : Type u_2} [inst_1 : CommMonoidWithZero R'] (f : Rˣ →* R'ˣ) (a : Rˣ),
(MulChar.equivToUnitHom.symm f) ↑a = ↑(f a)- Defined in
- Mathlib.NumberTheory.MulChar.Basic
- Cited by
- 6 results in Mathlib
- Foundations
- Depth 29 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- CommMonoidCommMonoidWithZero
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites11
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement · cited by 62,936
- Equivstatement · cited by 8,337
- Equiv.symmstatement · cited by 3,681
- MonoidHomstatement and proof · cited by 3,629
- Unitsstatement and proof · cited by 2,804
- CommMonoidstatement and proof · cited by 2,264
- Units.valstatement · cited by 1,966
- CommMonoidWithZerostatement and proof · cited by 913
- MulCharstatement · cited by 186
- MulChar.equivToUnitHomstatement · cited by 20
- MulChar.ofUnitHom_coeproof · cited by 1
Cited by6
Results whose statement or proof uses this declaration.
- DirichletCharacter.changeLevel_injectiveproof · cited by 5
- DirichletCharacter.changeLevel_eq_cast_of_dvdproof · cited by 3
- MulChar.domRestrict_ofUnitHomproof · cited by 2
- MulChar.exists_apply_ne_one_iff_exists_monoidHomproof · cited by 1
- MulChar.domRestrictHom_surjectiveproof · cited by 1
- MulChar.ofRootOfUnity_specproof · cited by 0