OAI/RepresentationTheory/FoulkesHowe/MultilinearDescent.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Problem346.multilinearDescend line 20

   Source documentation

   A multilinear map constant on the fibers of coordinatewise surjections descends.

   def multilinearDescend
       (q : ∀ i, M i →ₗ[R] N i) (hq : ∀ i, Surjective (q i))
       (f : MultilinearMap R M W)
       (hf : ∀ x y, (∀ i, q i (x i) = q i (y i)) → f x = f y) :
       MultilinearMap R N W where
   …

2. theorem OAI.Problem346.multilinearDescend_apply_image line 72
3. theorem OAI.Problem346.multilinearDescend_compLinearMap line 83