noZeroSMulDivisors — Mathlib

English

If α, β satisfy the NoZeroSmulDivisors assumption and α acts on β, then NoZeroSMulDivisors α (ι → β).

Русский

Если существуют предпосылки NoZeroSMulDivisors на α и β и α действует на β, то NoZeroSMulDivisors на α (ι → β).

LaTeX

$$$$\text{NoZeroSMulDivisors}(\alpha, \beta) \Rightarrow \text{NoZeroSMulDivisors}(\alpha, (\iota \to \beta)).$$$$

Lean4

/-- A special case of `Pi.noZeroSMulDivisors` for non-dependent types. Lean struggles to
synthesize this instance by itself elsewhere in the library. -/
instance _root_.Function.noZeroSMulDivisors {ι α β : Type*} [Zero α] [Zero β] [SMulWithZero α β]
    [NoZeroSMulDivisors α β] : NoZeroSMulDivisors α (ι → β) :=
  Pi.noZeroSMulDivisors _

Похожие утверждения