MonoidHom.exists_subfield_units_coe_eq
Source context 2 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.MonoidHom_exists_subfield_units_coe_eqLean source · statement
theorem _root_.MonoidHom.exists_subfield_units_coe_eq
{G : Type*} [Group G] {L : Type*} [Field L] (K : Subfield L)
(F : G →* G →* Lˣ) (hF : ∀ α β : G, ((F α β : Lˣ) : L) ∈ K) :
∃ F' : G →* G →* (↥K)ˣ, ∀ α β : G, (((F' α β : (↥K)ˣ) : ↥K) : L) = F α β