EtaleFundamentalGroups.Inertia.primeToRootsSeparableClosureLimitEquiv_scalar
The full comparison retains the literal included scalar at each exponent.
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace EtaleFundamentalGroups.Inertia
open ProCGroups.InverseSystems
universe u vLean source · statement
theorem primeToRootsSeparableClosureLimitEquiv_scalar
(k : Type u) (E : Type v) [Field k] [Field E] [Algebra k E]
(n : InvertibleExponent k)
(x : (primeToRootsSystem k (separableClosure k E)).inverseLimit) :
((primeToRootsSystem k E).projection n
((primeToRootsSeparableClosureLimitEquiv k E).toFun x)).val.val =
(((primeToRootsSystem k (separableClosure k E)).projection n x).val.val).val