Theorems · Theorem · commutative algebra
Algebra.norm_apply
∀ (R : Type u_1) {S : Type u_2} [inst : CommRing R] [inst_1 : Ring S] [inst_2 : Algebra R S] (x : S),
(Algebra.norm R) x = LinearMap.det ((Algebra.lmul R S) x)- Defined in
- Mathlib.RingTheory.Norm.Defs
- Cited by
- 8 results in Mathlib
- Foundations
- Depth 127 from the axioms · uses propext, Classical.choice, Quot.sound
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.
- DFunLike.coestatement · cited by 62,936
- RingHom.idstatement · cited by 18,349
- CommRingstatement and proof · cited by 17,173
- Algebrastatement and proof · cited by 11,388
- LinearMapstatement · cited by 10,215
- Ringstatement and proof · cited by 7,463
- MonoidHomstatement · cited by 3,629
- AlgHomstatement · cited by 3,236
- Module.Endstatement · cited by 774
- Algebra.normstatement · cited by 155
- LinearMap.detstatement · cited by 127
- Algebra.lmulstatement · cited by 41
Cited by8
Results whose statement or proof uses this declaration.
- Ideal.absNorm_span_singletonproof · cited by 18
- Algebra.norm_algebraMapproof · cited by 13
- Algebra.norm_eq_matrix_detproof · cited by 10
- Algebra.norm_normproof · cited by 5
- Algebra.norm_zeroproof · cited by 5
- Algebra.norm_algebraMap_of_basisproof · cited by 3
- Algebra.norm_eq_one_of_not_exists_basisproof · cited by 3
- ClassGroup.norm_leproof · cited by 1