Theorems · Theorem · commutative algebra
Algebra.norm_algebraMap
∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : Ring S] [inst_2 : Algebra R S] [Module.Free R S] (x : R),
(Algebra.norm R) ((algebraMap R S) x) = x ^ Module.finrank R SIf x is in the base ring R and S is free over R, then the norm is x ^ [S : R].
(If S is not finitely generated over R, then norm = 1 = x ^ 0 = x ^ (finrank R S).)
- Defined in
- Mathlib.RingTheory.Norm.Defs
- Cited by
- 13 results in Mathlib
- Foundations
- Depth 132 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites15
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement and proof · cited by 62,936
- CommRingstatement and proof · cited by 17,173
- Algebrastatement and proof · cited by 11,388
- RingHomstatement · cited by 10,189
- Ringstatement and proof · cited by 7,463
- Algebra.algebraMapstatement and proof · cited by 4,706
- MonoidHomstatement · cited by 3,629
- Module.finrankstatement and proof · cited by 1,770
- Module.Endproof · cited by 774
- Module.Freestatement and proof · cited by 597
- Algebra.normstatement · cited by 155
- LinearMap.detproof · cited by 127
Cited by13
Results whose statement or proof uses this declaration.
- IsCyclotomicExtension.discr_prime_pow_ne_twoproof · cited by 4
- Ideal.relNorm_algebraMapproof · cited by 4
- Ideal.spanIntNorm_localizationproof · cited by 3
- IsPrimitiveRoot.norm_eq_oneproof · cited by 3
- IsPrimitiveRoot.norm_pow_sub_one_twoproof · cited by 3
- X_pow_sub_C_irreducible_of_primeproof · cited by 2
- dvd_coeff_zero_of_aeval_eq_prime_smul_of_minpoly_isEisensteinAtproof · cited by 1
- RingOfIntegers.norm_algebraMapproof · cited by 1
- IsPrimitiveRoot.prime_dvd_of_dvd_norm_sub_oneproof · cited by 1
- Algebra.norm_natCastproof · cited by 1
- mem_adjoin_of_smul_prime_smul_of_minpoly_isEisensteinAtproof · cited by 1
- IsPrimitiveRoot.norm_eq_neg_one_powproof · cited by 1