English
The symmetry of domain congruence equals the domain-congruence with the symm of the equivalence.
Русский
Симметрия доменного конгруирования равна конгруированию домена со симметризацией эквивалентности.
LaTeX
$$domLCongr_symm : (domLCongr R N ι S e).symm = domLCongr R N ι S e.symm$$
Lean4
/-- Transfer the arguments to a map along an equivalence between argument indices.
This is the alternating version of `MultilinearMap.domDomCongr`. -/
@[simps]
def domDomCongr (σ : ι ≃ ι') (f : M [⋀^ι]→ₗ[R] N) : M [⋀^ι']→ₗ[R] N :=
{ f.toMultilinearMap.domDomCongr σ with
toFun := fun v => f (v ∘ σ)
map_eq_zero_of_eq' := fun v i j hv hij =>
f.map_eq_zero_of_eq (v ∘ σ) (i := σ.symm i) (j := σ.symm j) (by simpa using hv) (σ.symm.injective.ne hij) }
