Theorems · Definition · ring theory
QuadraticAlgebra.C
{R : Type u_1} → {a b : R} → [Zero R] → R → QuadraticAlgebra R a bThe natural function R → QuadraticAlgebra R a b.
Note that, if R is a ring, you should use algebraMap instead of C.
- Defined in
- Mathlib.Algebra.QuadraticAlgebra.Defs
- Cited by
- 22 results in Mathlib
- Foundations
- Depth 4 from the axioms · uses no axioms
- Assumes
- Zero
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- QuadraticAlgebrastatement · cited by 123
Cited by22
Results whose statement or proof uses this declaration.
- QuadraticAlgebra.C_injstatement · cited by 3
- QuadraticAlgebra.C_mul_eq_smulstatement · cited by 3
- QuadraticAlgebra.C_eq_algebraMapstatement · cited by 2
- QuadraticAlgebra.C_mulstatement · cited by 2
- QuadraticAlgebra.C_zerostatement · cited by 1
- QuadraticAlgebra.C_injectivestatement and proof · cited by 1
- QuadraticAlgebra.C_onestatement · cited by 1
- QuadraticAlgebra.C_substatement · cited by 0
- QuadraticAlgebra.re_Cstatement · cited by 0
- QuadraticAlgebra.smul_Cstatement and proof · cited by 0
- QuadraticAlgebra.isUnit_iff_norm_isUnitproof · cited by 0
- QuadraticAlgebra.im_Cstatement · cited by 0