noZeroSMulDivisors_finset — Mathlib

English

Specialized version of NoZeroSMulDivisors for Finset β with SMul α β.

Русский

Специализированная версия NoZeroSMulDivisors для Finset β с SMul α β.

LaTeX

$$$\text{NoZeroSMulDivisors }(α, Finset β)$$$

Lean4

instance noZeroSMulDivisors_finset [Zero α] [Zero β] [SMul α β] [NoZeroSMulDivisors α β] :
    NoZeroSMulDivisors α (Finset β) :=
  Function.Injective.noZeroSMulDivisors toSet coe_injective coe_zero coe_smul_finset

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