instFaithfulSMulProdOfNonempty — Mathlib

English

If Q and Λ are nonempty and D acts faithfully on Λ, then the regular wreath product D ≀ᵣ Q acts faithfully on Λ × Q.

Русский

Если Q и Λ непусты, и D действует достоверно на Λ, то регулярное вентовое произведение D ≀ᵣ Q действует достоверно на Λ × Q.

LaTeX

$$$ [Nonempty Q] [Nonempty \Lambda] : FaithfulSMul (D \wr_{\mathrm{r}} Q) (\Lambda \times Q) $$$

Lean4

instance [Nonempty Q] [Nonempty Λ] : FaithfulSMul (D ≀ᵣ Q) (Λ × Q) where
  eq_of_smul_eq_smul := by
    simp only [smul_def, Prod.mk.injEq, mul_left_inj, Prod.forall]
    intro m₁ m₂ h
    let ⟨a⟩ := ‹Nonempty Λ›
    let ⟨b⟩ := ‹Nonempty Q›
    ext q
    · have hh := fun a => (h a (m₁.right⁻¹ * q)).1
      rw [← (h a b).2] at hh
      group at hh
      exact FaithfulSMul.eq_of_smul_eq_smul hh
    · exact (h a b).2

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