Basis.induction_on

Stream: Is there code for X?

[Jireh Loreaux]

Do we have a way to do induction on a basis? That is, I would like to argue that if b : Basis ι R M and I have some predicate P : M → Prop that holds for the basis vectors and is closed under addition and scalar multiplication, then it holds on the entire module M. Note: I realize that I could say that x : M means x ∈ (⊤ : Submodule R M) which is x ∈ (span R (Set.range b)) and then do Submodule.induction_on, but I'm trying to avoid the hoop jumping.

[Eric Wieser]

I claim that usually the most effective hoops to jump through are the ones where you express P x as f x = g x for some morphisms f and g, then use docs#Basis.ext

[Andrew Yang]

apply Submodule.span_induction (b.mem_span x) should be what you need?

[Jireh Loreaux]

Eric, I don't think that approach works in my use case.