Zulip Chat Archive

Stream: general

Topic: variable inside header or outside header


view this post on Zulip Kenny Lau (Jul 25 2018 at 02:20):

import algebra.module
universes u v w u₁

namespace hidden1

variables {R : Type u} [comm_ring R]
include R

structure is_bilinear_map {M N P}
  [module R M] [module R N] [module R P]
  (f : M  N  P) : Prop :=
(add_pair :  x y z, f (x + y) z = f x z + f y z)
(pair_add :  x y z, f x (y + z) = f x y + f x z)
(smul_pair :  r x y, f (r  x) y = r  f x y)
(pair_smul :  r x y, f x (r  y) = r  f x y)

#check @is_bilinear_map
/-
is_bilinear_map :
  Π {R : Type u_1} [_inst_1 : comm_ring R] {M : Type u_2} {N : Type u_3} {P : Type u_4} [_inst_2 : module R M]
  [_inst_3 : module R N] [_inst_4 : module R P], (M → N → P) → Prop
-/

variables (M : Type v) (N : Type w) (P : Type u₁)
variables [module R M] [module R N] [module R P]

variables {f : M  N  P} (hf : is_bilinear_map f) --works

end hidden1

namespace hidden2

variables {R : Type u} [comm_ring R]
include R
variables (M : Type v) (N : Type w) (P : Type u₁)
variables [module R M] [module R N] [module R P]
variables {M N P}

structure is_bilinear_map (f : M  N  P) : Prop :=
(add_pair :  x y z, f (x + y) z = f x z + f y z)
(pair_add :  x y z, f x (y + z) = f x y + f x z)
(smul_pair :  r x y, f (r  x) y = r  f x y)
(pair_smul :  r x y, f x (r  y) = r  f x y)

#check @is_bilinear_map
/-
is_bilinear_map :
  Π {R : Type u_1} [_inst_1 : comm_ring R] {M : Type u_2} {N : Type u_3} {P : Type u_4}
  [_inst_2 : module R M (comm_ring.to_ring R)] [_inst_3 : module R N (comm_ring.to_ring R)]
  [_inst_4 : module R P (comm_ring.to_ring R)], (M → N → P) → Prop
-/

variables {f : M  N  P} (hf : is_bilinear_map f) -- fails

end hidden2

view this post on Zulip Kenny Lau (Jul 25 2018 at 02:21):

why does it make a difference whether the variables are inside or outside the header (the space between the name of the definition and the colon)?


Last updated: May 10 2021 at 00:31 UTC