equivalent quadratic forms

Stream: maths

[Johan Commelin]

What is the correct name for the new field in this structure:

structure equiv (Q₁ : quadratic_form R M₁) (Q₂ : quadratic_form R M₂) extends M₁ ≃ₗ[R] M₂ :=
(simil : ∀ m, Q₁ m = Q₂ (to_fun m))

[Mario Carneiro]

naturality?

[Mario Carneiro]

map_app? (maybe the other way around)