Module

RatFunc_exists_algEquiv_apply_X_eq_moebius.lean

Nyll.AlgebraicCurves.Foundations.Algebra.RatFunc_exists_algEquiv_apply_X_eq_moebius

2 declarations indexed from sourceView source ↗

Module documentation

Rat Func exists alg Equiv apply X eq moebius

Imports2

Mathlib.FieldTheory.RatFunc.AsPolynomial
Mathlib.FieldTheory.RatFunc.IntermediateField

Imported by2

theorem

moebius_aux

L33 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.RatFunc_exists_algEquiv_apply_X_eq_moebius.RatFunc.moebius_aux

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.RatFunc_exists_algEquiv_apply_X_eq_moebius
open Polynomial IntermediateField
namespace RatFunc
open _root_.RatFunc
open _root_.RatFunc
variable {K : Type*} [Field K]

Lean source · statement

theorem moebius_aux (a b c d : K) (hdet : a * d - b * c ≠ 0) :
    ∃ φ : RatFunc K ≃ₐ[K] RatFunc K,
      φ RatFunc.X = (RatFunc.C a * RatFunc.X + RatFunc.C b) / (RatFunc.C c * RatFunc.X + RatFunc.C
        d)

theorem

exists_algEquiv_apply_X_eq_moebius

L90 ↗

RatFunc.exists_algEquiv_apply_X_eq_moebius

Source context 3 commands