covariant_iff_contravariant — Mathlib

English

In a group N, Covariant N N (· * ·) r is equivalent to Contravariant N N (· * ·) r; i.e., covariance and contravariance coincide in groups.

Русский

В группе N ковариантность N N (· ·) r эквивалентна контравариантности; то есть в группах ковариантность и контравариантность совпадают.

LaTeX

$$Covariant N N (· * ·) r ↔ Contravariant N N (· * ·) r$$

Lean4

@[to_additive]
theorem covariant_iff_contravariant [Group N] : Covariant N N (· * ·) r ↔ Contravariant N N (· * ·) r :=
  by
  refine ⟨fun h a b c bc ↦ ?_, fun h a b c bc ↦ ?_⟩
  · rw [← inv_mul_cancel_left a b, ← inv_mul_cancel_left a c]
    exact h a⁻¹ bc
  · rw [← inv_mul_cancel_left a b, ← inv_mul_cancel_left a c] at bc
    exact h a⁻¹ bc

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