Structures · Algebra
ZeroHomClass
ZeroHomClass F M N states that F is a type of zero-preserving homomorphisms.
You should extend this typeclass when you extend ZeroHom.
- Defined in
- Mathlib.Algebra.Group.Hom.Defs
- Shape
- 3 explicit arguments · adds map_zero
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by2
Concrete types that are instances4
- ContinuousMapZero
- ZeroHom
- QuadraticMap
- AbsoluteValue
How is a type an instance?
Loading the hierarchy index…
Assumed by69
- map_zero
- map_eq_zero_iff
- map_ne_zero_iff
- norm_map
- HahnSeries.map
- EmbeddingLike.map_eq_zero_iff
- iterate_map_zero
- HahnSeries.map_coeff
- map_ne_zero_of_mem_nonZeroDivisors
- EmbeddingLike.map_ne_zero_iff
- nnnorm_map
- ZeroHomClass.map_zero
- Polynomial.gaussNorm_coe_powerSeries
- map_nonneg
- Polynomial.le_gaussNorm
- IsNonarchimedean.apply_natCast_le_one
- enorm_map
- DirectLimit.zero_def
- Polynomial.exists_eq_gaussNorm
- map_indicator
- ne_zero_of_map
- ZeroHomClass.toZeroHom
- Polynomial.gaussNorm_eq_zero_iff
- Matrix.map_single
- IsNonarchimedean.nsmul_le
- IsNonarchimedean.apply_sum_le
- Polynomial.gaussNorm_C
- ext_nat''
- ZeroHomClass.bound_of_antilipschitz
- IsNonarchimedean.nmul_le
- IsNonarchimedean.multiset_image_add
- Polynomial.gaussNorm_mul_le
- NeZero.of_map
- map_mem_nonZeroDivisors
- IsNonarchimedean.add_pow_le
- Polynomial.gaussNorm_monomial
- HahnSeries.map.congr_simp
- Finset.imageZeroHom
- Matrix.BlockTriangular.map
- IsNonarchimedean.apply_sum_univ_le
- DirectLimit.exists_eq_zero
- Finite.iSup_eq_iSup_subtype
- Finsupp.apply_single
- Filter.map_zero
- map_nonpos
- AddEquivClass.isDedekindFiniteAddMonoid_iff
- RatFunc.map_denom_ne_zero
- FunLike.monoidWithZero
- Polynomial.isNonarchimedean_gaussNorm
- PowerSeries.gaussNorm_monomial
Ancestors0
No ancestors.