Theorems · Definition · commutative algebra

Module.Relations.Solution.postcomp

{A : Type u} →
  [inst : Ring A] →
    {relations : Module.Relations A} →
      {M : Type v} →
        [inst_1 : AddCommGroup M] →
          [inst_2 : Module A M] →
            relations.Solution M →
              {N : Type v'} → [inst_3 : AddCommGroup N] → [inst_4 : Module A N] → (M →ₗ[A] N) → relations.Solution N

The image of a solution to relations : Relation A by a linear map M →ₗ[A] N.

Defined in: Mathlib.Algebra.Module.Presentation.Basic
Cited by: 17 results in Mathlib
Foundations: Depth 81 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: Ring AddCommGroup Module AddCommGroup Module

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites11

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

DFunLike.coeproof · cited by 62,936
Modulestatement and proof · cited by 20,661
RingHom.idstatement and proof · cited by 18,349
AddCommGroupstatement and proof · cited by 12,871
LinearMapstatement and proof · cited by 10,215
Ringstatement and proof · cited by 7,463
Module.Relations.Gproof · cited by 103
Module.Relationsstatement and proof · cited by 97
Module.Relations.Solutionstatement and proof · cited by 70
Module.Relations.Rproof · cited by 57
Module.Relations.Solution.varproof · cited by 39

Cited by30

Results whose statement or proof uses this declaration.

Module.Relations.Solution.IsPresentationCore.isPresentationproof · cited by 5
Module.Relations.Solution.IsPresentation.linearMapEquivproof · cited by 4
Module.Relations.Solution.postcomp_varstatement and proof · cited by 4
Module.Relations.Solution.IsPresentation.postcomp_descstatement · cited by 2
Module.Relations.Solution.directSumproof · cited by 2
Module.Relations.Solution.IsPresentationCore.mk.injstatement and proof · cited by 1
Module.Relations.Solution.IsPresentationCore.mk.noConfusionstatement and proof · cited by 1
Module.Relations.solutionFinsupp.isPresentationCoreproof · cited by 1
Module.Presentation.cokernelSolution.isPresentationCoreproof · cited by 1
Module.Relations.Solution.IsPresentation.postcomp_injectivestatement and proof · cited by 1
Module.Presentation.tautologicalSolutionIsPresentationCoreproof · cited by 1
Module.Relations.Solution.IsPresentationCore.downproof · cited by 1