Oliver Nash ocfnash

Deputy Director of Operations for Joint Systems Interdepartmental Operational Command

ocfnash / lie-semisimple-classification.lean

Last active July 22, 2021 13:02

	import algebra.lie.classical
	import algebra.lie.cartan_matrix
	import algebra.lie.semisimple
	import algebra.lie.direct_sum
	import field_theory.algebraic_closure
	open lie_algebra
	open_locale direct_sum
	notation L₁ ` ≅ₗ⁅` K `⁆ `L₂ := nonempty (L₁ ≃ₗ⁅K⁆ L₂)
	abbreviation sl (l : ℕ) (K : Type*) [field K] := special_linear.sl (fin l) K
	abbreviation sp (l : ℕ) (K : Type*) [field K] := symplectic.sp (fin l) K

ocfnash / render-dynkin.lean

Last active July 16, 2021 16:11

	import algebra.lie.cartan_matrix

	open widget

	variables {α : Type}

	namespace svg

	meta def fill : string → attr α
	\| s := attr.val "fill" $ s

ocfnash / compare_lie.py

Created February 10, 2021 17:33

Using `leancrawler` to aid review of https://github.com/leanprover-community/mathlib/pull/6141

	from leancrawler import LeanLib, LeanDeclGraph
	import re

	# lie_data_old = LeanLib.from_yaml('lie_data', '/Users/olivernash/Desktop/mathlib/src/algebra/lie/lie_data_old.yaml')
	# lie_data_old.dump('lie_data_old.dump')
	lie_data_old = LeanLib.load_dump('lie_data_old.dump')

	# lie_data_new = LeanLib.from_yaml('lie_data', '/Users/olivernash/Desktop/mathlib/src/algebra/lie/lie_data_new.yaml')
	# lie_data_new.dump('lie_data_new.dump')
	lie_data_new = LeanLib.load_dump('lie_data_new.dump')