AddEquiv.arrowCongr

{M : Type u_16} →
  {N : Type u_17} →
    {P : Type u_18} → {Q : Type u_19} → [inst : Add P] → [inst_1 : Add Q] → M ≃ N → P ≃+ Q → (M → P) ≃+ (N → Q)

An additive analogue of Equiv.arrowCongr, where the equivalence between the targets is additive.

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Results whose statement or proof uses this declaration.