domDomCongr_eq_zero_iff — Mathlib

English

Applying domDomCongr σ to an alternating map yields zero if and only if the map itself is zero.

Русский

Применение domDomCongr σ к чередующемуся отображению даёт нуль тогда и только тогда, когда само отображение равно нулю.

LaTeX

$$$f.domDomCongr(σ) = 0 \\iff f = 0$$$

Lean4

@[simp]
theorem domDomCongr_eq_zero_iff (σ : ι ≃ ι') (f : M [⋀^ι]→ₗ[R] N) : f.domDomCongr σ = 0 ↔ f = 0 :=
  (domDomCongrEquiv σ : M [⋀^ι]→ₗ[R] N ≃+ M [⋀^ι']→ₗ[R] N).map_eq_zero_iff

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