instNoZeroSMulDivisorsIntLocallyConstant

English

Nonzero integers act without zero divisors on LocallyConstant α ℤ.

Русский

Не нулевые целые влияют без сомножителей на LocallyConstant α ℤ.

LaTeX

$$$$\\text{NoZeroSMulDivisors} \\, \\mathbb{Z} \\; (\\mathrm{LocallyConstant}\\; \\alpha \\; \\mathbb{Z})$$$$

Lean4

instance (α : Type*) [TopologicalSpace α] : NoZeroSMulDivisors ℤ (LocallyConstant α ℤ) :=
  by
  constructor
  intro c f h
  rw [or_iff_not_imp_left]
  intro hc
  ext x
  apply mul_right_injective₀ hc
  simp [LocallyConstant.ext_iff] at h
  simpa [LocallyConstant.ext_iff] using h x

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