Theorems · Theorem · group theory
ZeroHom.mk.congr_simp
∀ {M : Type u_10} {N : Type u_11} [inst : Zero M] [inst_1 : Zero N] (toFun toFun_1 : M → N) (e_toFun : toFun = toFun_1)
(map_zero' : toFun 0 = 0), { toFun := toFun, map_zero' := map_zero' } = { toFun := toFun_1, map_zero' := ⋯ }- Defined in
- Mathlib.Algebra.Group.Equiv.TypeTags
- Cited by
- 20 results in Mathlib
- Foundations
- Depth 5 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- ZeroHomstatement · cited by 161
Cited by20
Results whose statement or proof uses this declaration.
- DirichletCharacter.LSeries_eulerProduct_exp_logproof · cited by 3
- Behrend.map_succproof · cited by 3
- tsum_dirichletSummandproof · cited by 2
- tsum_riemannZetaSummandproof · cited by 2
- toArithmeticFunction_congrproof · cited by 1
- DirichletCharacter.zetaMul_prime_pow_nonnegproof · cited by 1
- ValueDistribution.characteristic_sub_characteristic_inv_of_ne_zeroproof · cited by 1
- Function.locallyFinsuppWithin.logCounting_evenproof · cited by 1
- DirichletCharacter.isMultiplicative_toArithmeticFunctionproof · cited by 1
- ModularGroup.coe_truncatedFundamentalDomainproof · cited by 1
- UpperHalfPlane.norm_ρproof · cited by 0
- DirichletCharacter.LSeriesSummable_zetaMulproof · cited by 0