isAlt_iff_eq_neg_flip — Mathlib

English

Over a field with no zero divisors and char 0, B is alternating iff B = -B.flip.

Русский

В поле без делителей нуля и свойстве нуля хара, B чередующаяся тогда и только тогда, когда B = -B.flip.

LaTeX

$$$\text{NoZeroDivisors}(R) \land \text{CharZero}(R) \Rightarrow (\text{IsAlt}(B) \iff B = -B.flip)$$$

Lean4

theorem isAlt_iff_eq_neg_flip [NoZeroDivisors R] [CharZero R] {B : M₁ →ₛₗ[I] M₁ →ₛₗ[I] R} : B.IsAlt ↔ B = -B.flip :=
  by
  constructor <;> intro h
  · ext
    simp_rw [neg_apply, flip_apply]
    exact (h.neg _ _).symm
  intro x
  let h' := congr_fun₂ h x x
  simp only [neg_apply, flip_apply, ← add_eq_zero_iff_eq_neg] at h'
  exact add_self_eq_zero.mp h'

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