rename fields to align

JetBrains · Aug 10, 2024 · acfc723 · acfc723
1 parent 381e414
commit acfc723
Show file tree

Hide file tree

Showing 3 changed files with 11 additions and 11 deletions.
diff --git a/src/Algebra/Group/Representation/Category.ard b/src/Algebra/Group/Representation/Category.ard
@@ -58,8 +58,8 @@
   | ** (g : G) (e : KerLModule f) => (g A.** e.1, rewrite (f.func-**, e.2, B.g**-zro) idp)
   | **-assoc {_ _ : G} {_ : KerLModule f} => exts A.**-assoc
   | id-action => exts A.id-action
-  | lin => exts A.lin
-  | lin-*c => exts A.lin-*c
+  | **-ldistr => exts A.**-ldistr
+  | **-*c => exts A.**-*c
 
 
 \func KerLRepresHom {R : Ring} {G : Group} {A B : LRepres R G} (f : InterwiningMap A B) : InterwiningMap (KerLRepres f) A \cowith
@@ -71,8 +71,8 @@
   | ** (g : G) (e : ImageLModule f) => (g B.** e.1, TruncP.map e.2 \lam s => (g A.** s.1, func-** *> pmap (g B.**) s.2))
   | **-assoc => ext B.**-assoc
   | id-action => ext B.id-action
-  | lin => ext B.lin
-  | lin-*c => ext B.lin-*c
+  | **-ldistr => ext B.**-ldistr
+  | **-*c => ext B.**-*c
 
 
 

diff --git a/src/Algebra/Group/Representation/PermutationRepresentation.ard b/src/Algebra/Group/Representation/PermutationRepresentation.ard
@@ -23,8 +23,8 @@
   | LModule => Module
   | ** g f j => f (inverse g X.** j)
   | **-assoc => ext (\lam _ => rewrite (X.**-assoc, inverse_prod) idp)
-  | lin => idp
-  | lin-*c => ext (\lam _ => idp)
+  | **-ldistr => idp
+  | **-*c => ext (\lam _ => idp)
   | id-action => ext (\lam _ => rewrite (G.inverse_ide, X.id-action) idp)
   \where{
     \func inverse_prod {m n : G} : inverse (m * n) = inverse n * inverse m =>

diff --git a/src/Algebra/Group/Representation/Representation.ard b/src/Algebra/Group/Representation/Representation.ard
@@ -32,10 +32,10 @@
 -- also : https://www.maths.dur.ac.uk/users/jack.g.shotton/repthy/index.html
 
 \class LinRepres \extends LModule, GroupAction {
-  | lin {g :  G} {e e' : E} : g ** (e + e') = g ** e + g ** e'
-  | lin-*c {g :  G} {e : E} {c : R} : g ** (c *c e) = c *c (g ** e)
+  | **-ldistr {g :  G} {e e' : E} : g ** (e + e') = g ** e + g ** e'
+  | **-*c {g :  G} {e : E} {c : R} : g ** (c *c e) = c *c (g ** e)
 
-  \func g**-zro {g : G} : g ** 0 = 0 => rewrite (inv *c_zro-right, lin-*c, *c_zro-left, *c_zro-left) idp
+  \func g**-zro {g : G} : g ** 0 = 0 => rewrite (inv *c_zro-right, **-*c, *c_zro-left, *c_zro-left) idp
 }
 
 \func LRepres (R : Ring)(G : Group) : \Type => LinRepres {| R => R | G => G}
@@ -44,5 +44,5 @@
 \func TrivialAction {R : Ring}(E : LModule R)(G : Group) : LRepres R G \cowith
   | LModule => E
   | GroupAction => trivialAction G E
-  | lin-*c => idp
-  | lin => idp
+  | **-*c => idp
+  | **-ldistr => idp