transfer_def — Mathlib

English

Under the Sylow p-subgroup setup, for hg ∈ P, k ∈ N, and g0 ∈ G with conjugacy condition h, we have g0^{-1} g^k g0 = g^k.

Русский

В рамках подгруппы Силова P: если hg ∈ P, k ∈ ℕ и g0 ∈ G удовлетворяют условию сопряжения, то g0^{-1} g^k g0 = g^k.

LaTeX

$$$g_0^{-1} g^k g_0 = g^k$ under the stated hypotheses.$$

Lean4

@[to_additive]
theorem transfer_def [FiniteIndex H] (g : G) : transfer ϕ g = diff ϕ T (g • T) := by
  rw [transfer, ← diff_mul_diff, ← smul_diff_smul, mul_comm, diff_mul_diff] <;> rfl

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