theorem
L25 ↗correspondence_congr
AlgebraicCurve.Divisor.correspondence_congr
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Divisors.Proofs.Divisor_correspondence_congr
open IsDedekindDomain AlgebraicCurveLean source · statement
theorem _root_.AlgebraicCurve.Divisor.correspondence_congr {K F F₁ : Type*} [Field K] [Field F]
[Field F₁] [Algebra K F] [Algebra K F₁] [HasPrincipalDivisors K F₁] {φ ψ φ' ψ' : F →ₐ[K] F₁}
(hφeq : φ = φ') (hψeq : ψ = ψ') (hφ : φ.toRingHom.IsIntegral) (hψ : ψ.toRingHom.IsIntegral) (hφ'
: φ'.toRingHom.IsIntegral) (hψ' : ψ'.toRingHom.IsIntegral) (D : Divisor K F) :
Divisor.correspondence φ ψ hφ hψ D = Divisor.correspondence φ' ψ' hφ' hψ' D