Other results

Results named in the rest of Tau Ceti's TauCeti.RingTheory modules and in no roadmap's section, as Tau Ceti has them at commit ace60277.

Algebraic Hartogs principle for… to Krull–Akizuki for Mathlib's…

• Algebraic Hartogs principle for fractions
• The Auslander–Buchsbaum formula
• The Cauchy estimate at unit radius
• Chase–Harrison–Rosenberg (TauCeti.Algebra.isFiniteEtaleTorsor_iff)
• Chase–Harrison–Rosenberg (TauCeti.MulSemiringAction.tensorToPi_bijective)
• Chinese Remainder Theorem for AdjoinRoot
• Cramer's bound for subalgebras of integral elements
• Dedekind's different theorem, the tame case, as an exponent
• Euler's criterion in a finite residue domain
• The Frobenius surjectivity criterion
• The graded Nakayama lemma for generators
• The Hadamard three circles inequality on 𝕎 O[1/(p [ϖ])]
• Hazewinkel's functional equation lemma
• Hensel's lemma for the norm
• Hensel's lemma with a derivative dividing π ^ k
• Hensel's lemma without monicity
• Jacobi's formula
• The Jacobian criterion for étaleness
• Kedlaya's estimate (4.9.1) in the normalisation λ_ρ(p) = ρ
• Krull–Akizuki for Mathlib's integralClosure

Krull–Akizuki's length bound to Wedhorn's degree decomposition…

• Krull–Akizuki's length bound
• The Kummer–Dedekind irreducibility criterion
• The Leibniz kernel identity from a closed product functional
• Maschke's theorem after base change
• Nakayama's lemma for an idempotent
• Nakayama's lemma over ℤ
• The open mapping theorem over a Tate ring
• Serre's criterion for normality
• Serre's lemma
• Taylor's formula for polynomials
• Universality of Hazewinkel's formal group law over ℚ-algebras
• Wedhorn's degree decomposition, Lemma 8.33(i)

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.