Zulip Chat Archive

Stream: general

Topic: how to use linear combination


view this post on Zulip Blair Shi (Jul 23 2018 at 11:21):

variables {k : Type u} {V : Type v}
variable [field k]
variables [ring k] [module k V]
variables {a : k} {b : V}
include k
variables (x y : V)
variable (fvs : finite_dimensional_vector_space k V)

def is_in_vecsp (v : V) (fvs : finite_dimensional_vector_space k V) : Prop :=
v ∈ span {v₁ : V | v₁ ∈ fvs.ordered_basis}

lemma add_closed : is_in_vecsp x fvs ∧ is_in_vecsp y fvs → is_in_vecsp (x + y) fvs :=
begin
intro h₀,
cases h₀ with le ri,
have h₁ : ∃(lc₁ : lc k V), (∀ x∉fvs.ordered_basis, lc₁ x = 0) ∧ x = lc₁.sum (λb a, a • b), from le,

I don't know why for lc₁ in lc₁.sum (λb a, a • b), it reports

synthesized type class instance is not definitionally equal to expression inferred by typing rules, synthesized
  no_zero_divisors.to_has_zero k
inferred
  mul_zero_class.to_has_zero k

Can anyone help me to solve this problem?

view this post on Zulip Patrick Massot (Jul 23 2018 at 11:48):

Probably not until you give us a MWE (depending only on mathlib and not your own code).

view this post on Zulip Patrick Massot (Jul 23 2018 at 11:49):

You can use gist or pasteall if it's too long

view this post on Zulip Reid Barton (Jul 23 2018 at 14:00):

I think you should not have both field k and ring k

view this post on Zulip Kevin Buzzard (Jul 23 2018 at 19:58):

Yes -- try deleting the variable [field k] line and see if it works. If it doesn't, then follow Patrick's advice and post some code which will work for everyone, if possible.

view this post on Zulip Blair Shi (Jul 23 2018 at 22:13):

Yes, I deleted variable [field k]. now it works. Thx!


Last updated: May 13 2021 at 22:15 UTC