Structures · Algebra
SMulWithZero
SMulWithZero is a class consisting of a Type M₀ with 0 ∈ M₀ and a scalar multiplication
of M₀ on a Type A with 0, such that the equality r • m = 0 holds if at least one among r
or m equals 0.
- Shape
- 2 explicit arguments · adds zero_smul
Extends1
Extended by0
Nothing extends this class yet.
Concrete types that are instances7
- Int
- Nat
- Subtype
- OrderDual
- ULift
- MulOpposite
- Lex
How is a type an instance?
Loading the hierarchy index…
Assumed by167
- zero_smul
- Set.zero_smul_set
- HahnSeries.SummableFamily.smulFamily_toFun
- LinearIndependent.restrict_scalars'
- LaurentPolynomial.smeval
- Unitization.inr_mul
- HahnSeries.SummableFamily.smul
- Function.support_smul_subset_left
- smul_eq_zero_of_left
- Balanced.smul_mono
- Set.zero_smul_set_subset
- tsupport_smul_subset_left
- Filter.Tendsto.zero_smul_const
- LinearIndependent.restrict_scalars
- left_ne_zero_of_smul
- Set.subsingleton_zero_smul_set
- Unitization.isStarNormal_inr
- smul_nonpos_of_nonpos_of_nonneg
- Module.rank_top_le_rank_of_isScalarTower
- HahnSeries.SummableFamily.hasFiniteSupport_smul
- LaurentPolynomial.smeval_single
- HahnSeries.SummableFamily.smul_support_subset_prod
- smul_nonneg'
- Set.indicator_smul_const_apply
- Set.indicator_smul_apply_left
- HahnModule.support_smul_subset_vadd_support
- Finset.zero_smul_finset
- IsOrderedModule.of_smul_one_mono
- HahnModule.coeff_single_zero_smul
- HahnModule.zero_smul'
- starConvex_zero_iff
- pos_and_pos_or_neg_and_neg_of_smul_pos
- CFC.abs_smul_nonneg
- AddMonoidAlgebra.smul_eq
- HahnModule.coeff_smul_left
- HahnSeries.SummableFamily.smulFamily
- HahnModule.coeff_single_smul_vadd
- Balanced.smul_mem_mono
- neg_of_smul_pos_left
- HahnSeries.SummableFamily.smul_toFun
- Unitization.isIdempotentElem_inr_iff
- Set.indicator_smul_left
- Filter.zero_smul_filter_nonpos
- Unitization.IsIdempotentElem.inr
- neg_of_smul_neg_right
- HahnSeries.SummableFamily.sum_vAddAntidiagonal_eq
- PartitionOfUnity.continuous_smul
- PartitionOfUnity.continuous_finsum_smul
- AddMonoidAlgebra.smul_apply_addAction
- Function.HasFiniteSupport.smul_left