trans — Mathlib

English

If a divides b and a ∈ I, then b ∈ I.

Русский

Если a делит b и a ∈ I, то b ∈ I.

LaTeX

$$$\forall I\; (a,b: \alpha),\; (a \mid b) \rightarrow (a \in I) \rightarrow (b \in I).$$$

Lean4

@[stacks 00HX]
theorem trans (T : Type*) [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] [Algebra.HasGoingDown R S]
    [Algebra.HasGoingDown S T] : Algebra.HasGoingDown R T :=
  by
  rw [iff_generalizingMap_primeSpectrumComap, IsScalarTower.algebraMap_eq R S T]
  simp only [PrimeSpectrum.comap_comp, ContinuousMap.coe_comp]
  apply GeneralizingMap.comp
  · rwa [← iff_generalizingMap_primeSpectrumComap]
  · rwa [← iff_generalizingMap_primeSpectrumComap]

Похожие утверждения