Theorems · Theorem · commutative algebra
Algebra.norm_inv
∀ {K : Type u_4} [inst : Field K] {L : Type u_7} [inst_1 : DivisionRing L] [inst_2 : Algebra K L] [Module.Finite K L]
(x : L), (Algebra.norm K) x⁻¹ = ((Algebra.norm K) x)⁻¹- Defined in
- Mathlib.RingTheory.Norm.Basic
- Cited by
- 2 results in Mathlib
- Foundations
- Depth 134 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites13
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
- Algebrastatement and proof · cited by 11,388
- Fieldstatement and proof · cited by 7,404
- MonoidHomstatement · cited by 3,629
- DivisionRingstatement and proof · cited by 1,062
- Module.Finitestatement and proof · cited by 1,032
- map_oneproof · cited by 861
- inv_mul_cancel₀proof · cited by 267
- inv_zeroproof · cited by 184
- Algebra.normstatement and proof · cited by 155
- mul_left_injective₀proof · cited by 22
- Algebra.norm_zeroproof · cited by 5
Cited by2
Results whose statement or proof uses this declaration.
- groupCohomology.exists_div_of_norm_eq_oneproof · cited by 1
- Algebra.norm_zpowproof · cited by 0