Theorems · Inductive type · nonassociative algebras
NonUnitalSubalgebra
(R : Type u) → (A : Type v) → [inst : CommSemiring R] → [inst_1 : NonUnitalNonAssocSemiring A] → [Module R A] → Type v
A non-unital subalgebra is a sub(semi)ring that is also a submodule.
- Cited by
- 215 results in Mathlib
- Foundations
- Depth 2 from the axioms, rests on 8 definitions · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Modulestatement · cited by 20,661
- CommSemiringstatement · cited by 10,911
- NonUnitalNonAssocSemiringstatement · cited by 1,081
Cited by275
Results whose statement or proof uses this declaration.
- NonUnitalStarAlgebra.adjoinproof · cited by 43
- NonUnitalStarSubalgebra.toNonUnitalSubalgebrastatement · cited by 37
- NonUnitalSubalgebra.toNonUnitalSubsemiringstatement and proof · cited by 33
- NonUnitalAlgebra.adjoinstatement · cited by 33
- NonUnitalStarAlgHom.rangeproof · cited by 24
- NonUnitalSubalgebra.mapstatement and proof · cited by 23
- NonUnitalSubalgebra.toSubmodulestatement and proof · cited by 23
- NonUnitalStarSubalgebra.mapproof · cited by 23
- NonUnitalAlgebra.subset_adjoinstatement · cited by 13
- NonUnitalStarSubalgebra.topologicalClosureproof · cited by 12
- NonUnitalSubalgebra.centralizerstatement · cited by 12
- NonUnitalSubalgebra.inclusionstatement and proof · cited by 12
Showing the 200 most cited of 275.