All.lean
Nyll.AlgebraicCurves.Differentials.Kaehler.All
0 declarations indexed from sourceView source ↗
Imports7
- Nyll.AlgebraicCurves.Differentials.Kaehler.FunctionField
- Nyll.AlgebraicCurves.Differentials.Kaehler.Algebra_trace_inv_mul_derivation_eq_inv_norm_mul_derivation_norm
- Nyll.AlgebraicCurves.Differentials.Kaehler.Derivation_add_mulLeft_pow_char
- Nyll.AlgebraicCurves.Differentials.Kaehler.KaehlerDifferential_D_ne_zero_of_transcendental
- Nyll.AlgebraicCurves.Differentials.Kaehler.KaehlerDifferential_exists_unique_smul_D_of_transcendental
- Nyll.AlgebraicCurves.Differentials.Kaehler.KaehlerDifferential_span_D_eq_top_of_transcendental
- Nyll.AlgebraicCurves.Differentials.Kaehler.Weil
Imported by1
This module has no indexed declarations. Its imports and full source are available here.