Theorems · Definition · nonassociative algebras

NonUnitalAlgebra.gi

{R : Type u} →
  {A : Type v} →
    [inst : CommSemiring R] →
      [inst_1 : NonUnitalNonAssocSemiring A] →
        [inst_2 : Module R A] →
          [inst_3 : IsScalarTower R A A] →
            [inst_4 : SMulCommClass R A A] → GaloisInsertion (NonUnitalAlgebra.adjoin R) SetLike.coe

Galois insertion between adjoin and SetLike.coe.

Defined in: Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Cited by: 1 results in Mathlib
Foundations: Depth 71 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: CommSemiring NonUnitalNonAssocSemiring Module IsScalarTower SMulCommClass

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites12

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

Setstatement and proof · cited by 53,352
Modulestatement and proof · cited by 20,661
CommSemiringstatement and proof · cited by 10,911
SetLike.coestatement and proof · cited by 8,199
IsScalarTowerstatement and proof · cited by 3,896
SMulCommClassstatement and proof · cited by 1,927
NonUnitalNonAssocSemiringstatement and proof · cited by 1,081
NonUnitalSubalgebrastatement · cited by 215
GaloisInsertionstatement · cited by 35
NonUnitalAlgebra.adjoinstatement and proof · cited by 33
NonUnitalAlgebra.gcproof · cited by 5
NonUnitalSubalgebra.copyproof · cited by 3

Cited by1

Results whose statement or proof uses this declaration.

NonUnitalAlgHom.map_adjoinproof · cited by 1