Namespace KaehlerDifferential 8 theorems
- Nonvanishing of dx for a separating transcendental element
KaehlerDifferential.D_ne_zero_of_transcendental0 below · cited by 51 · depth 10 - Ω_{F/K} is spanned by dx for separating x
KaehlerDifferential.span_D_eq_top_of_transcendental0 below · cited by 19 · depth 10 - Unique coordinate of a differential along D x
KaehlerDifferential.exists_unique_smul_D_of_transcendental2 below · cited by 20 · depth 12 - Differentials of a local algebra with retraction are multiples of dt
KaehlerDifferential.exists_eq_smul_D_of_retraction_of_ker_le_span_sup_sq0 below · cited by 2 · depth 26 - Base change of differentials along a surjection
KaehlerDifferential.nonempty_baseChange_linearEquiv_quotient_span_tmul_D_of_surjective0 below · cited by 1 · depth 31 - Differentials of a localisation of A⊗_R B over A'
KaehlerDifferential.bijective_map_comp_mapBaseChange_of_isLocalization_tensorProduct0 below · cited by 2 · depth 32 - Jacobian presentation of Ω_{S/R} for a surjection from a polynomial ring
KaehlerDifferential.exists_linearMap_pi_surjective_ker_eq_span_pderiv_of_surjective0 below · cited by 1 · depth 34 - Non-p-th powers have non-zero absolute differential
KaehlerDifferential.D_ne_zero_of_forall_pow_ne0 below · cited by 1 · depth 35