Theorems · Theorem · commutative algebra
Algebra.FormallyUnramified.one_tmul_mul_elem
∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
[inst_3 : Algebra.FormallyUnramified R S] [inst_4 : Algebra.EssFiniteType R S] (s : S),
1 ⊗ₜ[R] s * Algebra.FormallyUnramified.elem R S = s ⊗ₜ[R] 1 * Algebra.FormallyUnramified.elem R S- Defined in
- Mathlib.RingTheory.Unramified.Finite
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 95 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites10
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CommRingstatement and proof · cited by 17,173
- Algebrastatement and proof · cited by 11,388
- TensorProductstatement and proof · cited by 2,545
- TensorProduct.tmulstatement and proof · cited by 1,182
- sub_eq_zeroproof · cited by 407
- sub_mulproof · cited by 170
- Algebra.FormallyUnramifiedstatement and proof · cited by 75
- Algebra.EssFiniteTypestatement and proof · cited by 68
- Algebra.FormallyUnramified.elemstatement and proof · cited by 6
- Algebra.FormallyUnramified.one_tmul_sub_tmul_one_mul_elemproof · cited by 1
Cited by1
Results whose statement or proof uses this declaration.
- Algebra.FormallyUnramified.finite_of_freeproof · cited by 7