Formalization of the existence of Frobenius elements

DOI10.1007/978-3-031-64529-7_7MaRDI QIDQ6637791zbMATH OpenFDO

Authors Jou Glasheen

Publication date 13 November 2024

Full work available at URL https://doi.org/10.1007/978-3-031-64529-7_7

zbMATH Keywords

AKLBFrobeniusLeanproof assistant

Mathematics Subject Classification ID

Formalization of mathematics in connection with theorem provers (68V20)

Cites work

• Engel's theorem in Mathlib
• Group cohomology in the Lean community library
• scientific article; zbMATH DE number 1703931 (Why is no real title available?)
• scientific article; zbMATH DE number 7622014 (Why is no real title available?)
• Number fields

This page was built for publication: Formalization of the existence of Frobenius elements

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6637791)