Module

ScalarRatioRigidity.lean

Nyll.GaloisCohomology.FieldTheory.ScalarRatioRigidity

1 declaration indexed from sourceView source ↗

Module documentation

Rigidity from scalar ratios

If every nonzero element of a field is carried to a scalar multiple of itself by scalars in a fixed proper subfield, a unital ring endomorphism is the identity. The proof compares an element outside the subfield with its translate by one.

Imports2

Mathlib.Algebra.Field.Subfield.Basic
Mathlib.Tactic.LinearCombination

Imported by2

theorem

ringHom_eq_id_of_div_mem_subfield

L24 ↗

FieldTheory.ringHom_eq_id_of_div_mem_subfield

Documentation

A field endomorphism which scales every element by an element of a fixed proper subfield is the identity.

Source context 2 commands

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

namespace FieldTheory
variable {K : Type*} [Field K]

Lean source · statement

theorem ringHom_eq_id_of_div_mem_subfield
    (C : Subfield K) (hC : C ≠ ⊤) (τ : K →+* K)
    (hratio : ∀ x : K, x ≠ 0 → τ x / x ∈ C) : τ = RingHom.id K

Module documentation

Rigidity from scalar ratios

Declarations

ringHom_eq_id_of_div_mem_subfield