Email Gateway (Aug 22 2022 at 20:35): Email Gateway (Aug 22 2022 at 20:35):From: José Manuel Rodríguez Caballero <josephcmac@gmail.com>
Hi,
I am defining the group GL(n, complex) in Isabelle/HOL (where n can be
infinite)
typedef (overloaded) ('a::complex_normed_vector) GL
= ‹{A::('a,'a) bounded. ∃ B. A *⇩o B = idOp ∧ B *⇩o A = idOp}›
It would be nice to have
instantiation GL :: (complex_normed_vector) group_mult
for some class of multiplicative groups, but I only found the class of
additive groups (group_add). So, my current instantiation is
instantiation GL :: (complex_normed_vector) group_add
From a formal point of view, it is fine, but the traditional notation for
GL(n, complex) is multiplicative rather than additive. Is there any
solution in order to work with GL(n, complex) using multiplicative notation?
Kind regards,
José M.
Email Gateway (Aug 22 2022 at 20:35):From: Akihisa Yamada <akihisayamada@nii.ac.jp>
Dear José,
one solution would be to instantiate up to comm_monoid_mult, and then
interpret locale Groups.group:
interpretation mult_GL: Groups.group
‹(*)::'a::complex_normed_vector GL ⇒ _› ‹1› ‹your_inverse› sorry
Then some lemmas are available, e.g., mult_GL.right_inverse.
Best regards,
Akihisa
Last updated: Apr 19 2024 at 12:27 UTC