specTensorTo_snd — Mathlib

English

Equality of two base compositions with SpecTensorTo.

Русский

Равенство двух оснований композиций с SpecTensorTo.

LaTeX

$$$(\text{Spec.map } T.tensorInl \circ X.fromSpecResidueField T.x) = (\text{Spec.map } T.tensorInr \circ Y.fromSpecResidueField T.y)$$$

Lean4

@[reassoc (attr := simp)]
theorem specTensorTo_snd : T.SpecTensorTo ≫ pullback.snd f g = Spec.map T.tensorInr ≫ Y.fromSpecResidueField T.y :=
  pullback.lift_snd _ _ _

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