Theorems · Theorem · group theory

Function.support_mul_of_ne_zero_right

∀ {ι : Type u_1} {M₀ : Type u_4} [inst : MulZeroClass M₀] [NoZeroDivisors M₀] (f : ι → M₀) {g : ι → M₀},
  (∀ (x : ι), g x ≠ 0) → (Function.support fun x => f x * g x) = Function.support f

If g is everywhere nonzero, then support (f * g) = support f.

Defined in

Mathlib.Algebra.GroupWithZero.Indicator

Cited by

0 results in Mathlib

Foundations

Depth 25 from the axioms · uses propext, Quot.sound

Assumes

MulZeroClassNoZeroDivisors