of_equiv' — Mathlib

English

A variant of of_equiv with explicit freeness assumption on P.

Русский

Вариант of_equiv с явной свободностью для P.

LaTeX

$$$$ \text{If } (\text{Module.Free } R P) \text{ and } e:\ P \simeq_\ R N, \mathrm{Module.Free } R N $$$$

Lean4

/-- A variation of `of_equiv`: the assumption `Module.Free R P` here is explicit rather than an
instance. -/
theorem of_equiv' {P : Type v} [AddCommMonoid P] [Module R P] (_ : Module.Free R P) (e : P ≃ₗ[R] N) : Module.Free R N :=
  of_equiv e

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