You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
structure bilin_form (R : Type u) (M : Type v) [ring R] [add_comm_group M] [module R M] :
Type (max u v)
bilin : M → M → R
bilin_add_left : ∀ (x y z : M), c.bilin (x + y) z = c.bilin x z + c.bilin y z
bilin_smul_left : ∀ (a : R) (x y : M), c.bilin (a • x) y = a * c.bilin x y
bilin_add_right : ∀ (x y z : M), c.bilin x (y + z) = c.bilin x y + c.bilin x z
bilin_smul_right :
when I expect
structure bilin_form (R : Type u) (M : Type v) [ring R] [add_comm_group M] [module R M] :
Type (max u v)
(bilin : M → M → R)
(bilin_add_left : ∀ (x y z : M), c.bilin (x + y) z = c.bilin x z + c.bilin y z)
(bilin_smul_left : ∀ (a : R) (x y : M), c.bilin (a • x) y = a * c.bilin x y)
(bilin_add_right : ∀ (x y z : M), c.bilin x (y + z) = c.bilin x y + c.bilin x z)
(bilin_smul_right : ∀ (a : R) (x y : M), c.bilin x (a • y) = a * c.bilin x y)
The text was updated successfully, but these errors were encountered:
On a structure such as https://leanprover-community.github.io/mathlib_docs/linear_algebra/bilinear_form.html#bilin_form the brackets surrounding each structure field are added via css, and on chrome do not copy when the whole block of text is selected for copy-paste.
I get
when I expect
The text was updated successfully, but these errors were encountered: