Zulip Chat Archive
Stream: maths
Topic: equivalent quadratic forms
Johan Commelin (May 21 2020 at 05:35):
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 (May 21 2020 at 05:50):
naturality?
Mario Carneiro (May 21 2020 at 05:52):
map_app? (maybe the other way around)
Last updated: Dec 20 2023 at 11:08 UTC