symm_map_smul

Stream: Is there code for X?

[Scott Carnahan]

I would like to contribute the following analogue of docs#MulEquiv.symm_map_mul but I don't know where to put it:

import Mathlib

lemma symm_map_smul {Γ Γ' P Q : Type*} [SMul Γ P] [SMul Γ' Q]
    (f : Γ ≃ Γ') (f₁ : P ≃ Q) (h : ∀ (x : Γ) (y : P), f₁ (x • y) = f x • f₁ y) (u : Γ') (v : Q) :
    f₁.symm (u • v) = f.symm u • f₁.symm v := by
  simpa [Equiv.symm_apply_apply f₁, Equiv.apply_symm_apply] using
    congrArg f₁.symm (h (f.symm u) (f₁.symm v)).symm

find_home! suggests a long list of low-level files, but none of them seem to fit well.

[Aaron Liu]

Why not state it for docs#MulActionSemiHomClass

[Aaron Liu]

import Mathlib.GroupTheory.GroupAction.Hom

@[to_additive EquivLike.inv_map_vaddₛₗ]
lemma EquivLike.inv_map_smulₛₗ {Γ Γ' P Q M F : Type*} [SMul Γ P] [SMul Γ' Q] [EquivLike M Γ Γ'] [EquivLike F P Q]
    (f : M) [MulActionSemiHomClass F f P Q] (f₁ : F) (u : Γ') (v : Q) :
    EquivLike.inv f₁ (u • v) = EquivLike.inv f u • EquivLike.inv f₁ v :=
  MulActionSemiHomClass.map_smulₛₗ (MulActionHom.inverse' f₁ (inv f₁)
    (EquivLike.right_inv f) (EquivLike.left_inv f₁) (EquivLike.right_inv f₁)) u v

[Scott Carnahan]

Thank you, that looks great! I was not aware of Equivlike.