Module

SemilinearAut_ofAlgAut_smul_place.lean

Nyll.AlgebraicCurves.Divisors.Semilinear.SemilinearAut_ofAlgAut_smul_place

2 declarations indexed from sourceView source ↗

Module documentation

Semilinear Aut of Alg Aut smul place

Imports1

Nyll.AlgebraicCurves.Divisors.Semilinear

Imported by4

theorem

solution

L26 ↗

AlgebraicCurves.Divisors.Semilinear.Proofs.SemilinearAut_ofAlgAut_smul_place.solution

Source context 3 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Divisors.Semilinear.Proofs.SemilinearAut_ofAlgAut_smul_place
open scoped Pointwise

Lean source · statement

theorem solution {K F : Type*} [Field K] [Field F] [Algebra K F] (σ : F ≃ₐ[K] F) (v :
  AlgebraicCurve.Place K F) : AlgebraicCurve.SemilinearAut.ofAlgAut σ • v = σ • v

theorem

ofAlgAut_smul_place

L42 ↗

AlgebraicCurve.SemilinearAut.ofAlgAut_smul_place

Source context 1 command