noZeroSMulDivisors — Mathlib

English

If α, β carry NoZeroSmulDivisors with SMul, then Finset α and Finset β inherit NoZeroSmulDivisors.

Русский

Если пары типов имеют NoZeroSmulDivisors, то Finset α и Finset β наследуют NoZeroSmulDivisors.

LaTeX

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

Lean4

instance noZeroSMulDivisors [Zero α] [Zero β] [SMul α β] [NoZeroSMulDivisors α β] :
    NoZeroSMulDivisors (Finset α) (Finset β) where
  eq_zero_or_eq_zero_of_smul_eq_zero
    {s t} := by exact_mod_cast eq_zero_or_eq_zero_of_smul_eq_zero (c := s.toSet) (x := t.toSet)

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