bijective_compr₂ₛₗ_of_equiv

English

A criterion for llcomp to be bijective: if f is bijective and g is bijective, then llcomp f g is bijective.

Русский

Критерий биективности llcomp: если f и g биективны, тогда llcomp f g биективен.

LaTeX

$$$\text{Bijective}(f) \land \text{Bijective}(g) \Rightarrow \text{Bijective}(\text{llcomp}(f,g)).$$$

Lean4

/-- A version of `Function.Bijective.comp` for composition of a bilinear map with a linear map. -/
theorem bijective_compr₂ₛₗ_of_equiv [RingHomInvPair σ₃₄ σ₄₃] [RingHomInvPair σ₄₃ σ₃₄] (f : M →ₛₗ[σ₁₃] N →ₛₗ[σ₂₃] P)
    (g : P ≃ₛₗ[σ₃₄] Q) (hf : Bijective f) : Bijective (f.compr₂ₛₗ g.toLinearMap) :=
  ⟨injective_compr₂ₛₗ_of_injective f g.toLinearMap hf.1 g.bijective.1, surjective_compr₂ₛₗ_of_equiv f g hf.2⟩

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