isAffineHom_isStableUnderBaseChange

English

IsAffineHom is stable under base change; proven from HasAffineProperty.

Русский

IsAffineHom сохраняется при базисном изменении; доказано через HasAffineProperty.

LaTeX

$$IsStableUnderBaseChange IsAffineHom$$

Lean4

instance isAffineHom_isStableUnderBaseChange : MorphismProperty.IsStableUnderBaseChange @IsAffineHom :=
  by
  apply HasAffineProperty.isStableUnderBaseChange
  letI := HasAffineProperty.isLocal_affineProperty
  apply AffineTargetMorphismProperty.IsStableUnderBaseChange.mk
  introv X hX H
  infer_instance

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